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

fix(tests/lean): adjust tests

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-02 12:51:20 -08:00
parent 3c564fcc55
commit befe41e8f5
2 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/axioms_of.lean
View file

@ -10,4 +10,4 @@ print axioms finset.union
print "-----" print "-----"
print axioms finset.mem print axioms finset.mem
print "-----" print "-----"
print axioms finset.union.comm print axioms finset.union_comm

12
tests/lean/simplifier_light.lean
View file

@ -46,18 +46,18 @@ attribute complement [light 2]
attribute union_comp_self [simp] attribute union_comp_self [simp]
lemma union_comp_self_left [simp] {X : Type} (s t : set X) : s ∪ (-s ∪ t)= univ := sorry lemma union_comp_self_left [simp] {X : Type} (s t : set X) : s ∪ (-s ∪ t)= univ := sorry
attribute union.comm [simp] attribute union_comm [simp]
attribute union.assoc [simp] attribute union_assoc [simp]
attribute union.left_comm [simp] attribute union_left_comm [simp]
#simplify eq env 0 x ∪ y ∪ z ∪ -x #simplify eq env 0 x ∪ y ∪ z ∪ -x
attribute inter_comp_self [simp] attribute inter_comp_self [simp]
lemma inter_comp_self_left [simp] {X : Type} (s t : set X) : s ∩ (-s ∩ t)= empty := sorry lemma inter_comp_self_left [simp] {X : Type} (s t : set X) : s ∩ (-s ∩ t)= empty := sorry
attribute inter.comm [simp] attribute inter_comm [simp]
attribute inter.assoc [simp] attribute inter_assoc [simp]
attribute inter.left_comm [simp] attribute inter_left_comm [simp]
#simplify eq env 0 x ∩ y ∩ z ∩ -x #simplify eq env 0 x ∩ y ∩ z ∩ -x