fix(tests/lean/interactive): adjust test to reflect changes in the standard library
This commit is contained in:
parent
ab873cfff9
commit
29aaa21f2a
1 changed files with 3 additions and 0 deletions
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue