michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean): adjust test to new eval semantics

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-10 21:10:33 -08:00
parent 4ebd3e2c27
commit e2ce942513
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/eta_bug.lean.expected.out
View file

@ -1 +1 @@
λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.rec H₁ H₂