diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 205f8335b3..95c86899cc 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -201,6 +201,10 @@ macro_rules
     else
       `(%[ $elems,* | List.nil ])
 
+-- TODO: should be `infix:50 " matches " => fun e p => match e with | p => true | _ => false`
+macro:50 e:term:51 " matches " p:term:51 : term =>
+  `(match $e:term with | $p:term => true | _ => false)
+
 namespace Parser.Tactic
 syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic
 syntax (name := intros) "intros " (colGt (ident <|> "_"))* : tactic