From 29aaa21f2a662dfccbd7331d3c91e5ac762b02b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Dec 2014 19:53:41 -0800 Subject: [PATCH] fix(tests/lean/interactive): adjust test to reflect changes in the standard library --- tests/lean/interactive/findp.input.expected.out | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out index 4ffb70e7f6..a7644b6778 100644 --- a/tests/lean/interactive/findp.input.expected.out +++ b/tests/lean/interactive/findp.input.expected.out @@ -11,9 +11,12 @@ false.decidable|decidable false false.induction_on|∀ (C : Prop), false → C true_ne_false|¬ true = false eq.false_elim|?p = false → ¬ ?p +not_of_is_false|is_false ?c → ¬ ?c p_ne_false|?p → ?p ≠ false +is_false|Π (c : Prop) [H : decidable c], Prop decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2 not_false|¬ false +of_not_is_false|¬ is_false ?c → ?c if_false|∀ (t e : ?A), ite false t e = e iff.false_elim|?a ↔ false → ¬ ?a -- ENDFINDP