fix(tests): fix tests after port

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

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)

tests/lean/770.hlean.expected.out

@@ -1,2 +1,2 @@
-770.hlean:17:14: error: function expected at
+770.hlean:16:18: error: function expected at
-  0
+  n

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

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) :=
+definition inverse_id [instance] {a : A} : is_iso (id' a) :=
-is_iso.mk (id a) (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
 

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,

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

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

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,
+  injection H with p,
-  rewrite e_1
+  rewrite p
 end
 
 example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) :

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
 

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)