From 0f81c2e65b70644c453a9a25020b6887687ac974 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Tue, 16 Feb 2016 22:00:29 -0500 Subject: [PATCH] fix(tests/lean/noncomp_theory,simlifier_light): fix tests --- tests/lean/noncomp_theory.lean.expected.out | 2 +- tests/lean/simplifier_light.lean | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/lean/noncomp_theory.lean.expected.out b/tests/lean/noncomp_theory.lean.expected.out index 03fea7cda..dfa6026e4 100644 --- a/tests/lean/noncomp_theory.lean.expected.out +++ b/tests/lean/noncomp_theory.lean.expected.out @@ -1,4 +1,4 @@ -noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.real_has_div' +noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.discrete_linear_ordered_field' noncomputable definition g : ℝ → ℝ → ℝ := λ (a : ℝ), div (a + a) definition r : ℕ → ℕ := diff --git a/tests/lean/simplifier_light.lean b/tests/lean/simplifier_light.lean index 4fcc5922b..c27c58734 100644 --- a/tests/lean/simplifier_light.lean +++ b/tests/lean/simplifier_light.lean @@ -40,10 +40,10 @@ namespace s open set universe l constants (A : Type.{l}) (x y z v w : set A) -attribute complement [light 2] +attribute compl [light 2] -- TODO(dhs, leo): Where do we put this group of simp rules? -attribute union_comp_self [simp] +attribute union_compl_self [simp] lemma union_comp_self_left [simp] {X : Type} (s t : set X) : s ∪ (-s ∪ t)= univ := sorry attribute union_comm [simp] @@ -52,8 +52,8 @@ 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_compl_self [simp] +lemma inter_compl_self_left [simp] {X : Type} (s t : set X) : s ∩ (-s ∩ t)= empty := sorry attribute inter_comm [simp] attribute inter_assoc [simp]