From 7000365a0434ac1f0f919e87b15f89cb211ec120 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 28 Nov 2014 23:03:37 -0800
Subject: [PATCH] fix(tests/lean): to reflect changes in the standard library

---
 tests/lean/run/class_bug1.lean |  2 +-
 tests/lean/run/class_bug2.lean |  2 +-
 tests/lean/run/rel.lean        | 15 +--------------
 3 files changed, 3 insertions(+), 16 deletions(-)

diff --git a/tests/lean/run/class_bug1.lean b/tests/lean/run/class_bug1.lean
index 6f41d9deb..ecf0af9a3 100644
--- a/tests/lean/run/class_bug1.lean
+++ b/tests/lean/run/class_bug1.lean
@@ -20,7 +20,7 @@ context sec_cat
   parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
   definition compose := rec (λ comp id assoc idr idl, comp) Cat
   definition id := rec (λ comp id assoc idr idl, id) Cat
-  infixr `∘`:60 := compose
+  infixr ∘ := compose
   inductive is_section {A B : ob} (f : mor A B) : Type :=
   mk : ∀g, g ∘ f = id → is_section f
 end sec_cat
diff --git a/tests/lean/run/class_bug2.lean b/tests/lean/run/class_bug2.lean
index 2ef67428f..120c729e0 100644
--- a/tests/lean/run/class_bug2.lean
+++ b/tests/lean/run/class_bug2.lean
@@ -20,6 +20,6 @@ section sec_cat
   variables {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
   definition compose := rec (λ comp id assoc idr idl, comp) Cat
   definition id := rec (λ comp id assoc idr idl, id) Cat
-  infixr `∘`:60 := compose
+  infixr ∘ := compose
 end sec_cat
 end category
diff --git a/tests/lean/run/rel.lean b/tests/lean/run/rel.lean
index bcc221ce0..0a78b06eb 100644
--- a/tests/lean/run/rel.lean
+++ b/tests/lean/run/rel.lean
@@ -2,24 +2,11 @@ import logic algebra.relation
 open relation
 
 namespace is_equivalence
-  inductive cls {T : Type} (R : T → T → Type) : Prop :=
+  inductive cls {T : Type} (R : T → T → Prop) : Prop :=
   mk : is_reflexive R → is_symmetric R → is_transitive R → cls R
 
-  theorem is_reflexive {T : Type} {R : T → T → Type} {C : cls R} : is_reflexive R :=
-  cls.rec (λx y z, x) C
-
-  theorem is_symmetric {T : Type} {R : T → T → Type} {C : cls R} : is_symmetric R :=
-  cls.rec (λx y z, y) C
-
-  theorem is_transitive {T : Type} {R : T → T → Type} {C : cls R} : is_transitive R :=
-  cls.rec (λx y z, z) C
-
 end is_equivalence
 
-instance is_equivalence.is_reflexive
-instance is_equivalence.is_symmetric
-instance is_equivalence.is_transitive
-
 theorem and_inhabited_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
 iff.intro (take Hab, and.elim_right Hab) (take Hb, and.intro Ha Hb)