From 2edf91ce4243e59cfdd5f54b5e71f7841e462404 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Dec 2015 08:40:21 -0800 Subject: [PATCH] fix(tests/lean/interactive/findp): broken test output --- tests/lean/interactive/findp.input.expected.out | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out index feda13f33..5380295b9 100644 --- a/tests/lean/interactive/findp.input.expected.out +++ b/tests/lean/interactive/findp.input.expected.out @@ -14,6 +14,7 @@ false.cases_on|Π (C : Type), false → C false.induction_on|∀ (C : Prop), false → C false_of_true_iff_false|(true ↔ false) → false true_ne_false|¬true = false +simplifier.unit_simp.false_imp|false → ?A ↔ true nat.lt_self_iff_false|∀ (n : ℕ), n < n ↔ false iff_false|∀ (a : Prop), a ↔ false ↔ ¬a true_iff_false|true ↔ false ↔ false @@ -24,6 +25,7 @@ not_of_iff_false|(?a ↔ false) → ¬?a is_false|Π (c : Prop) [H : decidable c], Prop classical.eq_true_or_eq_false|∀ (a : Prop), a = true ∨ a = false classical.eq_false_or_eq_true|∀ (a : Prop), a = false ∨ a = true +simplifier.unit_simp.not_true_of_false|¬true ↔ false nat.lt_zero_iff_false|∀ (a : ℕ), a < 0 ↔ false not_of_eq_false|?p = false → ¬?p nat.succ_le_self_iff_false|∀ (n : ℕ), nat.succ n ≤ n ↔ false