diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 5dd1e4b9b7..b20ed8aeac 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -106,7 +106,9 @@ withPosition $ fun pos => (if optionalFirstBar then optional "| " else "| ") >> sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|") -@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts +def matchDiscr := optIdent >> termParser + +@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts @[builtinTermParser] def «nomatch» := parser!:leadPrec "nomatch " >> termParser def optExprPrecedence := optional (try ":" >> termParser maxPrec) @[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser