From bae919355e523bd2c6733ab1fda79e0829f19782 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 9 Jun 2021 19:20:33 +0200
Subject: [PATCH] feat: `matches`

---
 src/Init/Notation.lean | 4 ++++
 1 file changed, 4 insertions(+)

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