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

fix: tacticSeqBracketed

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-28 16:24:27 -07:00
parent 2755972447
commit d4c1432574
2 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -24,7 +24,7 @@ namespace Tactic
def tacticSeq1Indented : Parser :=
parser! many1Indent $ tacticParser >> optional "; "
def tacticSeqBracketed : Parser :=
parser! "{" >> sepBy tacticParser "; " true >> "}"
parser! "{" >> many (tacticParser >> optional "; ") >> "}"
def tacticSeq :=
nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented

9
tests/lean/run/newfrontend1.lean
View file

@ -160,6 +160,15 @@ case b => exact y
traceState
repeat assumption
theorem simple13b (x y z : Nat) : y = z → x = x → x = y → x = z := by {
intros h1 h2 h3;
traceState;
apply @Eq.trans;
case b => exact y;
traceState;
repeat assumption
}
theorem simple14 (x y z : Nat) : y = z → x = x → x = y → x = z := by
intros
apply @Eq.trans