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

chore: fix calc test

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-25 06:59:46 -07:00
parent f9fd0b3de4
commit 42f1e16f44
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/calc.lean
View file

@ -4,7 +4,7 @@ variable (pf12 : t1 = t2) (pf23 : t2 = t3) (pf34 : t3 = t4)
theorem foo : t1 = t4 :=
calc
t1 = t2 := pf12
_ = t3 := id
_ = t3 := pf23
_ = t4 := pf34
variable (t5 : Nat)