michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/eta_bug.lean.expected.out
Leonardo de Moura 33f18b9454 fix(kernel/converter): remove buggy eta-reduction and rely only on eta-expansion 
The bug is exposed by new unit test
2014-10-21 16:54:25 -07:00

1 line
74 B
Text
Raw Blame History

λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
Reference in a new issue View git blame Copy permalink