From ea7470375fcf610a36114375e8e4e6023471fe84 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Nov 2014 18:44:36 -0800
Subject: [PATCH] fix(tests/lean): to reflect changes in the standard library

---
 tests/lean/interactive/calc_assistant.input    | 17 -----------------
 .../calc_assistant.input.expected.out          | 10 ----------
 tests/lean/print_ax2.lean.expected.out         |  2 +-
 tests/lean/run/imp_bang.lean                   | 18 ------------------
 tests/lean/run/print.lean                      |  4 ++--
 5 files changed, 3 insertions(+), 48 deletions(-)
 delete mode 100644 tests/lean/interactive/calc_assistant.input
 delete mode 100644 tests/lean/interactive/calc_assistant.input.expected.out
 delete mode 100644 tests/lean/run/imp_bang.lean

diff --git a/tests/lean/interactive/calc_assistant.input b/tests/lean/interactive/calc_assistant.input
deleted file mode 100644
index b7802b86f..000000000
--- a/tests/lean/interactive/calc_assistant.input
+++ /dev/null
@@ -1,17 +0,0 @@
-VISIT calc_assistant.lean
-SYNC 13
-import logic algebra.category.basic
-open eq eq.ops category functor natural_transformation
-variables {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
-protected definition compose2 (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
-natural_transformation.mk
-  (λ a, η a ∘ θ a)
-  (λ a b f, calc
-    H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc
-                  ... = (η b ∘ G f) ∘ θ a : naturality η f
-                  ... = η b ∘ (G f ∘ θ a) :
-                            assoc
-                  ... = η b ∘ (θ b ∘ F f) : naturality θ f
-                  ... = (η b ∘ θ b) ∘ F f : assoc)
-WAIT
-INFO 11
diff --git a/tests/lean/interactive/calc_assistant.input.expected.out b/tests/lean/interactive/calc_assistant.input.expected.out
deleted file mode 100644
index 42da28ead..000000000
--- a/tests/lean/interactive/calc_assistant.input.expected.out
+++ /dev/null
@@ -1,10 +0,0 @@
--- BEGINWAIT
--- ENDWAIT
--- BEGININFO
--- TYPE|11|28
-η b ∘ G f ∘ θ a = (η b ∘ G f) ∘ θ a
--- ACK
--- IDENTIFIER|11|28
-category.assoc
--- ACK
--- ENDINFO
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
index 199efe96c..5ade5f5fa 100644
--- a/tests/lean/print_ax2.lean.expected.out
+++ b/tests/lean/print_ax2.lean.expected.out
@@ -1,2 +1,2 @@
-funext : ∀ {A : Type} {B : A → Type} {f g : Π (x : A), B x}, (∀ (x : A), f x = g x) → f = g
+funext : ∀ {A : Type} {B : A → Type} {f g : Π (a : A), B a}, (∀ (a : A), f a = g a) → f = g
 strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A), (∃ (x : A), P x) → P x }
diff --git a/tests/lean/run/imp_bang.lean b/tests/lean/run/imp_bang.lean
deleted file mode 100644
index 074558d96..000000000
--- a/tests/lean/run/imp_bang.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import logic algebra.category.basic
-open eq eq.ops category functor natural_transformation
-
-
-variables {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
-protected definition compose2 (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
-natural_transformation.mk
-  (λ a, η a ∘ θ a)
-  (λ a b f, calc
-    H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc
-                  ... = (η b ∘ G f) ∘ θ a : naturality η f
-                  ... = η b ∘ (G f ∘ θ a) : assoc
-                  ... = η b ∘ (θ b ∘ F f) : naturality θ f
-                  ... = (η b ∘ θ b) ∘ F f : assoc)
-
-theorem tst (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
-calc a  = b : H₁
-    ... = c : H₂
diff --git a/tests/lean/run/print.lean b/tests/lean/run/print.lean
index b6af55c7b..95d491db7 100644
--- a/tests/lean/run/print.lean
+++ b/tests/lean/run/print.lean
@@ -1,10 +1,10 @@
 import data.num logic data.prod data.nat data.int algebra.category.basic
-open num prod int nat category functor
+open num prod int nat category
 
 print instances inhabited
 print raw 3+2
 print options
-print coercions functor
+print coercions Category
 print "-----------"
 print coercions
 print "-----------"