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

feat: add match tactic parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-27 15:57:05 -07:00
parent 7a6effa54f
commit d2f9f250db
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/Lean/Parser/Tactic.lean
View file

@ -49,6 +49,10 @@ def generalizingVars := optional (" generalizing " >> many1 ident)
@[builtinTacticParser] def «induction» := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
@[builtinTacticParser] def «cases» := parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
def withIds : Parser := optional (" with " >> many1 ident')
def matchAlt : Parser := group (sepBy1 termParser ", " >> darrow >> tacticParser)
def matchAlts : Parser := withPosition $ fun pos => (optional "| ") >> sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
@[builtinTacticParser] def «match» := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
@[builtinTacticParser] def paren := parser! "(" >> nonEmptySeq >> ")"
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"