From f495fa04c87f873ea59909a597a8b5edbe169f3e Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 9 Dec 2015 00:11:11 -0500
Subject: [PATCH] fix(tests): fix tests after port

---
 tests/lean/608.hlean.expected.out                  | 12 ++++++------
 tests/lean/770.hlean                               |  2 +-
 tests/lean/770.hlean.expected.out                  |  4 ++--
 tests/lean/hott/cases_eq.hlean                     |  2 +-
 tests/lean/hott/class_loop.hlean                   |  8 ++++----
 tests/lean/hott/constr_tac.hlean                   |  2 +-
 tests/lean/hott/contra1.hlean                      |  8 ++++----
 tests/lean/hott/disable_instances.hlean            |  2 +-
 tests/lean/hott/inj_tac.hlean                      |  4 ++--
 tests/lean/hott/len_eq.hlean                       |  3 ---
 tests/lean/hott/notation_with_nested_tactics.hlean |  2 +-
 11 files changed, 23 insertions(+), 26 deletions(-)

diff --git a/tests/lean/608.hlean.expected.out b/tests/lean/608.hlean.expected.out
index a329abe91..d28192a5d 100644
--- a/tests/lean/608.hlean.expected.out
+++ b/tests/lean/608.hlean.expected.out
@@ -1,11 +1,11 @@
+definition id [reducible] : Π {A : Type}, A → A :=
+λ (A : Type) (a : A), a
+
 definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a :=
 ID
-
-definition function.id [reducible] : Π {A : Type}, A → A :=
-λ (A : Type) (a : A), a
 -----------
+definition id [reducible] : Π {A : Type}, A → A
+λ (A : Type) (a : A), a
+
 definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a
 ID
-
-definition function.id [reducible] : Π {A : Type}, A → A
-λ (A : Type) (a : A), a
diff --git a/tests/lean/770.hlean b/tests/lean/770.hlean
index 7808bc067..d501464bf 100644
--- a/tests/lean/770.hlean
+++ b/tests/lean/770.hlean
@@ -12,7 +12,7 @@ open nat unit equiv eq
 
 
   definition encode (n m : ℕ) : (n = m) ≃ code n m :=
-  equiv.MK (λp, sorry) -- p ▸ refl n)
+  equiv.MK (λp, p ▸ refl n)
            (match n m with
             | 0 0 := sorry
             end)
diff --git a/tests/lean/770.hlean.expected.out b/tests/lean/770.hlean.expected.out
index d187d7d4f..cd9389f01 100644
--- a/tests/lean/770.hlean.expected.out
+++ b/tests/lean/770.hlean.expected.out
@@ -1,2 +1,2 @@
-770.hlean:17:14: error: function expected at
-  0
+770.hlean:16:18: error: function expected at
+  n
diff --git a/tests/lean/hott/cases_eq.hlean b/tests/lean/hott/cases_eq.hlean
index b2dc9c8cc..bcd6673ec 100644
--- a/tests/lean/hott/cases_eq.hlean
+++ b/tests/lean/hott/cases_eq.hlean
@@ -1,4 +1,4 @@
-open eq.ops
+open eq
 
 theorem trans {A : Type} {a b c : A} (h₁ : a = b) (h₂ : b = c) : a = c :=
 begin
diff --git a/tests/lean/hott/class_loop.hlean b/tests/lean/hott/class_loop.hlean
index 3a221648b..e0a11ce25 100644
--- a/tests/lean/hott/class_loop.hlean
+++ b/tests/lean/hott/class_loop.hlean
@@ -1,6 +1,6 @@
 constant (A : Type₁)
 constant (hom : A → A → Type₁)
-constant (id : Πa, hom a a)
+constant (id' : Πa, hom a a)
 
 structure is_iso [class] {a b : A} (f : hom a b) :=
 (inverse : hom b a)
@@ -9,8 +9,8 @@ open is_iso
 set_option pp.metavar_args true
 set_option pp.purify_metavars false
 
-definition inverse_id [instance] {a : A} : is_iso (id a) :=
-is_iso.mk (id a) (id a)
+definition inverse_id [instance] {a : A} : is_iso (id' a) :=
+is_iso.mk (id' a) (id' a)
 
 definition inverse_is_iso [instance] {a b : A} (f : hom a b) (H : is_iso f) : is_iso (@inverse a b f H) :=
 is_iso.mk (inverse f) f
@@ -19,7 +19,7 @@ constant a : A
 
 set_option trace.class_instances true
 
-definition foo := inverse (id a)
+definition foo := inverse (id' a)
 
 set_option pp.implicit true
 
diff --git a/tests/lean/hott/constr_tac.hlean b/tests/lean/hott/constr_tac.hlean
index 0f1903182..23a045192 100644
--- a/tests/lean/hott/constr_tac.hlean
+++ b/tests/lean/hott/constr_tac.hlean
@@ -22,7 +22,7 @@ end
 
 open nat
 
-example (a : nat) : a > 0 → Σ x, x > 0 :=
+example (a : nat) : a > 0 → Σ(x : ℕ), x > 0 :=
 begin
   intro Ha,
   existsi a,
diff --git a/tests/lean/hott/contra1.hlean b/tests/lean/hott/contra1.hlean
index b39aa9a6c..3cf9260f5 100644
--- a/tests/lean/hott/contra1.hlean
+++ b/tests/lean/hott/contra1.hlean
@@ -1,16 +1,16 @@
+open eq
+
 example (a b : nat) (h : empty) : a = b :=
 by contradiction
 
 example : ∀ (a b : nat), empty → a = b :=
 by contradiction
 
-example : ∀ (a b : nat), 0 = 1 → a = b :=
+example : ∀ (a b : nat), 0 = 1 :> ℕ → a = b :=
 by contradiction
 
-definition id {A : Type} (a : A) := a
-
 example : ∀ (a b : nat), id empty → a = b :=
 by contradiction
 
-example : ∀ (a b : nat), id (0 = 1) → a = b :=
+example : ∀ (a b : nat), id (0 = 1 :> ℕ) → a = b :=
 by contradiction
diff --git a/tests/lean/hott/disable_instances.hlean b/tests/lean/hott/disable_instances.hlean
index 1f0b71cf1..1b9c0bad4 100644
--- a/tests/lean/hott/disable_instances.hlean
+++ b/tests/lean/hott/disable_instances.hlean
@@ -7,7 +7,7 @@ definition H : is_equiv f := sorry
 definition loop [instance] [h : is_equiv f] : is_equiv f :=
 h
 
-example (a : A) : let H' : is_equiv f := H in @(inv f) H' (f a) = a :=
+example (a : A) : let H' : is_equiv f := H in @(is_equiv.inv f) H' (f a) = a :=
 begin
   with_options [elaborator.ignore_instances true] (apply left_inv f a)
 end
diff --git a/tests/lean/hott/inj_tac.hlean b/tests/lean/hott/inj_tac.hlean
index 5e776fa76..e3e92a3a3 100644
--- a/tests/lean/hott/inj_tac.hlean
+++ b/tests/lean/hott/inj_tac.hlean
@@ -12,8 +12,8 @@ notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
 example (a b : nat) : succ a = succ b → a + 2 = b + 2 :=
 begin
   intro H,
-  injection H,
-  rewrite e_1
+  injection H with p,
+  rewrite p
 end
 
 example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) :
diff --git a/tests/lean/hott/len_eq.hlean b/tests/lean/hott/len_eq.hlean
index 33414d181..a3a4ea436 100644
--- a/tests/lean/hott/len_eq.hlean
+++ b/tests/lean/hott/len_eq.hlean
@@ -62,9 +62,6 @@ definition heq.trans : ∀ {A B C : Type} {a : A} {b : B} {c : C}, a == b → b
 theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
 | A A (eq.refl A) a := ⟨eq.refl A, eq.refl a⟩
 
-definition default (A : Type) [H : inhabited A] : A :=
-inhabited.rec_on H (λ a, a)
-
 definition lem_eq (A : Type) : Type :=
 ∀ (n m : nat) (v : vector A n) (w : vector A m), v == w → n = m
 
diff --git a/tests/lean/hott/notation_with_nested_tactics.hlean b/tests/lean/hott/notation_with_nested_tactics.hlean
index 97967a67b..d33eb3257 100644
--- a/tests/lean/hott/notation_with_nested_tactics.hlean
+++ b/tests/lean/hott/notation_with_nested_tactics.hlean
@@ -9,5 +9,5 @@ h
 
 notation `noinstances` t:max := by+ with_options [elaborator.ignore_instances true] (exact t)
 
-example (a : A) : let H' : is_equiv f := H in @(inv f) H' (f a) = a :=
+example (a : A) : let H' : is_equiv f := H in @(is_equiv.inv f) H' (f a) = a :=
 noinstances (left_inv f a)