From befe41e8f51dd0ac07164093a8bff8e24a0ebc35 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Jan 2016 12:51:20 -0800 Subject: [PATCH] fix(tests/lean): adjust tests --- tests/lean/axioms_of.lean | 2 +- tests/lean/simplifier_light.lean | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/lean/axioms_of.lean b/tests/lean/axioms_of.lean index 2ff97f522..9adad7a53 100644 --- a/tests/lean/axioms_of.lean +++ b/tests/lean/axioms_of.lean @@ -10,4 +10,4 @@ print axioms finset.union print "-----" print axioms finset.mem print "-----" -print axioms finset.union.comm +print axioms finset.union_comm diff --git a/tests/lean/simplifier_light.lean b/tests/lean/simplifier_light.lean index 703f8ea14..4fcc5922b 100644 --- a/tests/lean/simplifier_light.lean +++ b/tests/lean/simplifier_light.lean @@ -46,18 +46,18 @@ attribute complement [light 2] attribute union_comp_self [simp] lemma union_comp_self_left [simp] {X : Type} (s t : set X) : s ∪ (-s ∪ t)= univ := sorry -attribute union.comm [simp] -attribute union.assoc [simp] -attribute union.left_comm [simp] +attribute union_comm [simp] +attribute union_assoc [simp] +attribute union_left_comm [simp] #simplify eq env 0 x ∪ y ∪ z ∪ -x attribute inter_comp_self [simp] lemma inter_comp_self_left [simp] {X : Type} (s t : set X) : s ∩ (-s ∩ t)= empty := sorry -attribute inter.comm [simp] -attribute inter.assoc [simp] -attribute inter.left_comm [simp] +attribute inter_comm [simp] +attribute inter_assoc [simp] +attribute inter_left_comm [simp] #simplify eq env 0 x ∩ y ∩ z ∩ -x