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

chore: fix test

Browse source
This commit is contained in:
Gabriel Ebner 2022-09-16 14:43:19 +02:00 • committed by Leonardo de Moura
parent ca4dfa5627
commit 0e01d855b0
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/lean/traceTacticSteps.lean.expected.out
View file

@ -18,17 +18,14 @@
[Elab.step] focus
apply And.intro✝
with_annotate_state"<;>" skip
all_goals
trivial
all_goals trivial
[Elab.step]
apply And.intro✝
with_annotate_state"<;>" skip
all_goals
trivial
all_goals trivial
[Elab.step]
apply And.intro✝
with_annotate_state"<;>" skip
all_goals
trivial
all_goals trivial
[Elab.step] apply And.intro✝
[Elab.step] apply True.intro✝