From e2ce94251324b5829d6cdc5213db3b6844639b68 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Nov 2014 21:10:33 -0800 Subject: [PATCH] fix(tests/lean): adjust test to new `eval` semantics --- tests/lean/eta_bug.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/eta_bug.lean.expected.out b/tests/lean/eta_bug.lean.expected.out index acdb9c4c2..6ce8ac64d 100644 --- a/tests/lean/eta_bug.lean.expected.out +++ b/tests/lean/eta_bug.lean.expected.out @@ -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₂