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

feat: allow h : annotation on match discriminants

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-10 10:12:24 -07:00
parent c8ab63ea75
commit 3ce794c58a
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Parser/Term.lean
View file

@ -106,7 +106,9 @@ withPosition $ fun pos =>
(if optionalFirstBar then optional "| " else "| ") >>
sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
def matchDiscr := optIdent >> termParser
@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@[builtinTermParser] def «nomatch» := parser!:leadPrec "nomatch " >> termParser
def optExprPrecedence := optional (try ":" >> termParser maxPrec)
@[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser