From 912c5254def32faa550079f03e2574e8fcb6faa8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Jan 2016 16:37:33 -0800 Subject: [PATCH] fix(tests/lean/run/cases_bug): adjust test to changes in the std lib --- tests/lean/run/cases_bug.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/cases_bug.lean b/tests/lean/run/cases_bug.lean index 706df951a..76f4f91c6 100644 --- a/tests/lean/run/cases_bug.lean +++ b/tests/lean/run/cases_bug.lean @@ -1,4 +1,4 @@ import logic.cast -theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a +theorem cast_heq₂ : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a | A A (eq.refl A) a := heq_of_eq !cast_eq