fix(tests/lean/interactive/findp): adjust test
This commit is contained in:
parent
93a0f62cd3
commit
e580e6cdb1
1 changed files with 1 additions and 0 deletions
|
@ -9,6 +9,7 @@ false.rec_on|Π (C : Type), false → C
|
|||
false_iff_true|false ↔ true ↔ false
|
||||
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
|
||||
nat.lt_self_iff_false|∀ (n : ℕ), n < n ↔ false
|
||||
true_iff_false|true ↔ false ↔ false
|
||||
|
|
Loading…
Reference in a new issue