diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 9db9c85116..ca7faf17c2 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -77,6 +77,9 @@ def bracktedBinder (requireType := false) := explicitBinder requireType <|> impl
 @[builtinTermParser] def depArrow := parser! bracktedBinder true >> unicodeSymbolCheckPrec " → " " -> " 25 >> termParser
 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
+@[builtinTermParser] def «nomatch» := parser! "nomatch " >> termParser
 
 def namedArgument  := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
 @[builtinTermParser] def app   := tparser! pushLeading >> (namedArgument <|> termParser appPrec)
diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean
index 12c847300e..3604e79ef6 100644
--- a/tests/playground/termparsertest1.lean
+++ b/tests/playground/termparsertest1.lean
@@ -74,7 +74,11 @@ test [
 "f (x : a) -> b",
 "f ((x : a) -> b)",
 "(f : (n : Nat) → Vector Nat n) -> Nat",
-"∀ x y (z : Nat), x > y -> x > y - z"
+"∀ x y (z : Nat), x > y -> x > y - z",
+"
+match x with
+| some x => true
+| none => false"
 ];
 testFailures [
 "f {x : a} -> b",