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