From 1c484e8926766dc28b03373200eaba26e5675c10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Nov 2016 12:23:36 -0800
Subject: [PATCH] chore(tests/lean/run): adjust tests

---
 tests/lean/run/assoc_flat.lean | 2 --
 tests/lean/run/rw_set1.lean    | 3 ---
 2 files changed, 5 deletions(-)

diff --git a/tests/lean/run/assoc_flat.lean b/tests/lean/run/assoc_flat.lean
index 5632870fcc..4d4a472dba 100644
--- a/tests/lean/run/assoc_flat.lean
+++ b/tests/lean/run/assoc_flat.lean
@@ -1,7 +1,5 @@
 open tactic expr
 
-constant nat.add_assoc (a b c : nat) : (a + b) + c = a + (b + c)
-
 meta definition is_op_app (op : expr) (e : expr) : option (expr × expr) :=
 match e with
 | (app (app fn a1) a2) := if op = fn then some (a1, a2) else none
diff --git a/tests/lean/run/rw_set1.lean b/tests/lean/run/rw_set1.lean
index 37f971f97c..d94265eab6 100644
--- a/tests/lean/run/rw_set1.lean
+++ b/tests/lean/run/rw_set1.lean
@@ -1,6 +1,3 @@
-constant nat.add_assoc (a b c : nat) : (a + b) + c = a + (b + c)
-
-
 namespace foo
   attribute [simp] nat.add_assoc
   print nat.add_assoc