From 383c0d6d4c403d79c5576b99274ddcad6c7c943d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Feb 2015 14:08:37 -0800 Subject: [PATCH] fix(tests/lean/interactive/findp): adjust test to reflect recent changes in the standard library --- tests/lean/interactive/findp.input.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out index 8d73bf38f..bdb578364 100644 --- a/tests/lean/interactive/findp.input.expected.out +++ b/tests/lean/interactive/findp.input.expected.out @@ -6,7 +6,6 @@ false.rec|Π (C : Type), false → C false.of_ne|?a ≠ ?a → false false.rec_on|Π (C : Type), false → C false.cases_on|Π (C : Type), false → C -false.decidable|decidable false false.induction_on|∀ (C : Prop), false → C true_ne_false|¬ true = false not_of_is_false|is_false ?c → ¬ ?c @@ -16,5 +15,6 @@ is_false|Π (c : Prop) [H : decidable c], Prop not_of_eq_false|?p = false → ¬ ?p decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2 not_false|¬ false +decidable_false|decidable false of_not_is_false|¬ is_false ?c → ?c -- ENDFINDP