From 0a018f2369fa8edbd3dd6c47819c643d5cb145fa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Apr 2021 18:38:44 -0700
Subject: [PATCH] chore: add support for `binop%` in patterns

---
 src/Lean/Elab/Match.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 23ebca691f..ea6aa6cff1 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -387,6 +387,10 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     let pat := stx[2]
     let pat ← collect pat
     `(_root_.namedPattern $id $pat)
+  else if k == ``Lean.Parser.Term.binop then
+    let lhs ← collect stx[2]
+    let rhs ← collect stx[3]
+    return stx.setArg 2 lhs |>.setArg 3 rhs
   else if k == ``Lean.Parser.Term.inaccessible then
     return stx
   else if k == strLitKind then