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

feat: injection tactic notation

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-08 10:34:39 -07:00
parent 5ea1160e86
commit a708c5d134
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Parser/Tactic.lean
View file

@ -45,6 +45,8 @@ def usingRec : Parser := optional (" using " >> ident)
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')
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
@[builtinTacticParser] def paren := parser! "(" >> nonEmptySeq >> ")"
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"