From a379d2db5e75129138c4e616c3dbc5a66e847bf8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 23 Jun 2021 13:58:41 +0200
Subject: [PATCH] refactor: simplify `matches` implementation

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

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 95c86899cc..b99901f18c 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -201,9 +201,7 @@ 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)
+notation:50 e:51 " matches " p:51 => match e with | p => true | _ => false
 
 namespace Parser.Tactic
 syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic