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

feat: populate builtinTacticSeqParser with tacticSeq

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-03 10:26:51 -08:00
parent 775096a820
commit c88d0c8a8c
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/Basic.lean
View file

@ -256,7 +256,7 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
stx[0].getSepArgs.forM evalTactic
@[builtinTactic paren] def evalParen : Tactic := fun stx =>
evalSeq1 stx[1]
evalTactic stx[1]
@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := fun stx =>
stx[0].forArgsM fun seqElem => evalTactic seqElem[0]

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

@ -13,6 +13,8 @@ namespace Tactic
builtin_initialize
registerBuiltinParserAttribute `builtinTacticSeqParser `tacticSeq
@[builtinTacticSeqParser] def tacticSeqElem := tacticSeq
def underscoreFn : ParserFn := fun c s =>
let s := symbolFn "_" c s;
let stx := s.stxStack.back;
@ -79,7 +81,7 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match
def withIds : Parser := optional (" with " >> many1 (checkColGt >> ident'))
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
@[builtinTacticParser] def paren := parser! "(" >> seq1 >> ")"
@[builtinTacticParser] def paren := parser! "(" >> tacticSeq >> ")"
@[builtinTacticParser] def nestedTactic := tacticSeqBracketed
@[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1