diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 0eed4057c3..cc646d9b73 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -78,7 +78,8 @@ def bracktedBinder (requireType := false) := explicitBinder requireType <|> impl def simpleBinder := parser! many1 binderIdent @[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracktedBinder) >> ", " >> termParser def equation := parser! " | " >> sepBy1 termParser ", " >> " => " >> termParser -@[builtinTermParser] def «match» := parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> many1 equation +def equations : Parser := withPosition $ fun pos => many1 (checkColGe pos.column "'match' cases must be indented" >> equation) +@[builtinTermParser] def «match» := parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> equations @[builtinTermParser] def «nomatch» := parser! "nomatch " >> termParser def namedArgument := tparser! try ("(" >> ident >> " := ") >> termParser >> ")" diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean index 3604e79ef6..3b1b9dcf57 100644 --- a/tests/playground/termparsertest1.lean +++ b/tests/playground/termparsertest1.lean @@ -78,7 +78,14 @@ test [ " match x with | some x => true -| none => false" +| none => false", +" +match x with +| some y => match y with + | some (a, b) => a + b + | none => 1 +| none => 0 +" ]; testFailures [ "f {x : a} -> b",