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

fix: withIds parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-29 18:50:08 -07:00
parent 0f3bd8abb4
commit 6670378907
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -73,7 +73,7 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match
@[builtinTacticParser] def «match» := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
@[builtinTacticParser] def «introMatch» := parser! nonReservedSymbol "intro " >> matchAlts
def withIds : Parser := optional (" with " >> many1 ident')
def withIds : Parser := optional (" with " >> many1 (checkColGt >> ident'))
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
@[builtinTacticParser] def paren := parser! "(" >> seq1 >> ")"
@[builtinTacticParser] def nestedTactic := tacticSeqBracketed