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

chore: add proper kind for tacticSeq1Indented

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-28 15:42:36 -07:00
parent aa410283c6
commit 85d8c4fa85
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Parser/Term.lean
View file

@ -22,12 +22,12 @@ categoryParser `tactic rbp
namespace Tactic
def tacticSeq1Indented : Parser :=
node `Lean.Parser.Tactic.seq $ withPosition $
parser! withPosition $
sepBy1 tacticParser (try ("; " >> checkColGe "tatic must be indented"))
def tacticSeqBracketed : Parser :=
parser! "{" >> sepBy tacticParser "; " true >> "}"
parser! "{" >> sepBy tacticParser "; " true >> "}"
def tacticSeq :=
nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
/- Raw sequence for quotation and grouping -/
def seq1 :=