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

fix(library/logic/examples/instances_test): we do not support the set_option class.conservative false anymore

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-18 16:14:12 -07:00
parent 97407eb178
commit 9348701a5b
1 changed files with 0 additions and 5 deletions

5
library/logic/examples/instances_test.lean
View file

@ -14,11 +14,6 @@ open eq.ops
example (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
set_option class.conservative false
example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
subst iff H1 H2
/-
exit
example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=