fix: match pattern missing test

src/Lean/Elab/PatternVar.lean

@@ -159,6 +159,19 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     discard <| processVar h
     ``(_root_.namedPattern $id $pat $h)
   else if k == ``Lean.Parser.Term.binop then
+    /-
+    We support `binop%` syntax in patterns because we
+    wanted to support `x+1` in patterns.
+    Recall that the `binop%` syntax was added to improve elaboration of some binary operators: `+` is one of them.
+    Recall that `HAdd.hAdd` is marked as `[match_pattern]`
+    TODO for a distant future: make this whole procedure extensible.
+    -/
+    -- Check whether the `binop%` operator is marked with `[match_pattern]`,
+    -- We must check that otherwise Lean will accept operators that are not tagged with this annotation.
+    let some (.const fName _) ← resolveId? stx[1] "pattern"
+      | throwCtorExpected
+    unless hasMatchPatternAttribute (← getEnv) fName do
+      throwCtorExpected
     let lhs ← collect stx[2]
     let rhs ← collect stx[3]
     return stx.setArg 2 lhs |>.setArg 3 rhs

tests/lean/binop_at_pattern_issue.lean

@@ -0,0 +1,5 @@
+open Std BitVec
+def f4 (v : Std.BitVec 32) : Nat :=
+  match v with
+  | 10#20 ++ 0#12  => 0 -- Should be rejected since `++` does not have `[match_pattern]`
+  | _ => 1

tests/lean/binop_at_pattern_issue.lean.expected.out

@@ -0,0 +1 @@
+binop_at_pattern_issue.lean:4:4-4:17: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected