max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: matches

Browse source
This commit is contained in:
Sebastian Ullrich 2021-06-09 19:20:33 +02:00 • committed by Leonardo de Moura
parent 459e2e8cea
commit bae919355e
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Notation.lean
View file

@ -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