fix: missing atomic at match_expr parser

src/Lean/Parser/Do.lean

@@ -160,7 +160,7 @@ def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
 
 def doMatchExprAlts := ppDedent <| matchExprAlts (rhsParser := doSeq)
 def optMetaFalse :=
-  optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ")
+  optional (atomic ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") "))
 @[builtin_doElem_parser] def doMatchExpr := leading_parser:leadPrec
   "match_expr " >> optMetaFalse >> termParser >> " with" >> doMatchExprAlts
 

tests/lean/run/match_expr_meta_modifier.lean

@@ -0,0 +1,13 @@
+import Lean
+
+open Lean Meta
+
+def f1 (e : Expr) : MetaM Expr := do
+  match_expr (← whnf e) with
+  | And a b => mkAppM ``And #[b, a]
+  | _ => return e
+
+def f2 (e : Expr) : MetaM Expr := do
+  match_expr (meta := false) (← whnf e) with
+  | And a b => mkAppM ``And #[b, a]
+  | _ => return e