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

fix: add SyntaxNodeKind for seq

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-16 11:25:24 -08:00
parent 7a65c13800
commit 5122d88527
1 changed files with 4 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -19,24 +19,22 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
@[inline] def tacticParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
categoryParser `tactic rbp
def tacticSeq {k : ParserKind} : Parser k :=
sepBy1 tacticParser "; " true
namespace Tactic
def seq := parser! sepBy1 tacticParser "; " true
@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> optional ident
@[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many ident
@[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
@[builtinTacticParser] def «apply» := parser! nonReservedSymbol "apply " >> termParser
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> tacticSeq >> "end"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> tacticSeq >> "}"
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
@[builtinTacticParser] def orelse := tparser! pushLeading >> " <|> " >> tacticParser 1
end Tactic
namespace Term
@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> tacticSeq >> "end"
@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> Tactic.seq >> "end"
end Term