From 657b508cdf37e32dfcee9807d8fa4dab6e1047eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Dec 2015 22:42:31 -0800 Subject: [PATCH] fix(tests/lean/simplifier_light): adjust test --- tests/lean/simplifier_light.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/simplifier_light.lean b/tests/lean/simplifier_light.lean index 3227ea847..703f8ea14 100644 --- a/tests/lean/simplifier_light.lean +++ b/tests/lean/simplifier_light.lean @@ -3,8 +3,8 @@ -- when there is a proof obligation. import algebra.ring algebra.field data.set data.finset open algebra -attribute neg [light 2] -attribute inv [light 2] +attribute neg [light 3] +attribute inv [light 3] attribute add.right_inv [simp] attribute add_neg_cancel_left [simp] @@ -40,7 +40,7 @@ namespace s open set universe l constants (A : Type.{l}) (x y z v w : set A) -attribute complement [light 1] +attribute complement [light 2] -- TODO(dhs, leo): Where do we put this group of simp rules? attribute union_comp_self [simp]