michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/interactive/findp): broken test output

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-04 08:40:21 -08:00
parent 8c431bdb20
commit 2edf91ce42
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/interactive/findp.input.expected.out
View file

@ -14,6 +14,7 @@ false.cases_on|Π (C : Type), false → C
false.induction_on|∀ (C : Prop), false → C false.induction_on|∀ (C : Prop), false → C
false_of_true_iff_false|(true ↔ false) → false false_of_true_iff_false|(true ↔ false) → false
true_ne_false|¬true = false true_ne_false|¬true = false
simplifier.unit_simp.false_imp|false → ?A ↔ true
nat.lt_self_iff_false|∀ (n : ℕ), n < n ↔ false nat.lt_self_iff_false|∀ (n : ℕ), n < n ↔ false
iff_false|∀ (a : Prop), a ↔ false ↔ ¬a iff_false|∀ (a : Prop), a ↔ false ↔ ¬a
true_iff_false|true ↔ false ↔ false 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 is_false|Π (c : Prop) [H : decidable c], Prop
classical.eq_true_or_eq_false|∀ (a : Prop), a = true ∨ a = false classical.eq_true_or_eq_false|∀ (a : Prop), a = true ∨ a = false
classical.eq_false_or_eq_true|∀ (a : Prop), a = false ∨ a = true 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 nat.lt_zero_iff_false|∀ (a : ℕ), a < 0 ↔ false
not_of_eq_false|?p = false → ¬?p not_of_eq_false|?p = false → ¬?p
nat.succ_le_self_iff_false|∀ (n : ℕ), nat.succ n ≤ n ↔ false nat.succ_le_self_iff_false|∀ (n : ℕ), nat.succ n ≤ n ↔ false