fix(tests/lean/run): adjust tests

tests/lean/run/coe13.lean

@@ -21,10 +21,9 @@ check g (functor.to_fun f) 0
 
 check g f 0
 
-definition id (A : Type) (a : A) := a
 
 constant S : struct
 constant a : S
 
-check id (struct.to_sort S) a
-check id S a
+check @id (struct.to_sort S) a
+check @id S a

tests/lean/run/contra1.lean

@@ -9,8 +9,6 @@ by contradiction
 example : ∀ (a b : nat), (0:nat) = 1 → a = b :=
 by contradiction
 
-definition id {A : Type} (a : A) := a
-
 example : ∀ (a b : nat), id false → a = b :=
 by contradiction
 

tests/lean/run/div2.lean

@@ -1,6 +1,6 @@
 import logic data.nat.sub algebra.relation data.prod
 
-open nat relation relation.iff_ops prod
+open nat relation prod
 open decidable
 open eq.ops
 

tests/lean/run/rel.lean

@@ -1,23 +0,0 @@
-import logic algebra.relation
-open relation
-
-namespace is_equivalence
-  inductive cls {T : Type} (R : T → T → Prop) : Prop :=
-  mk : is_reflexive R → is_symmetric R → is_transitive R → cls R
-
-end is_equivalence
-
-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)
-
-theorem test (a b c : Prop) (P : Prop → Prop) (H1 : a ↔ b) (H2 : c ∧ a) : c ∧ b :=
-iff.subst H1 H2
-
-theorem test2 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : Q ↔ (S ∧ Q) :=
-iff.symm (and_inhabited_left Q H1)
-
-theorem test3 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : R ↔ (S ∧ Q) :=
-iff.subst (test2 Q R S H3 H1) H3
-
-theorem test4 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : R ↔ (S ∧ Q) :=
-iff.subst (iff.symm (and_inhabited_left Q H1)) H3

tests/lean/run/section2.lean

@@ -2,9 +2,7 @@ import data.nat
 
 section foo
   variable A : Type
-  definition id (a : A) := a
   variable a : nat
-  check _root_.id nat a
 end foo
 
 namespace n1

tests/lean/run/tactic4.lean

@@ -1,7 +1,6 @@
 import logic
 open tactic (renaming id->id_tac)
 
-definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A
 := by unfold id; assumption

tests/lean/run/tactic5.lean

@@ -1,8 +1,6 @@
 import logic
 open tactic (renaming id->id_tac)
 
-definition id {A : Type} (a : A) := a
-
 infixl `;`:15 := tactic.and_then
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A

tests/lean/run/tactic6.lean

@@ -1,8 +1,6 @@
 import logic
 open tactic (renaming id->id_tac)
 
-definition id {A : Type} (a : A) := a
-
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A
 := by unfold id; assumption
 

tests/lean/run/vars_anywhere.lean

@@ -1,7 +1,5 @@
 variable {A : Type}
 
-definition id (a : A) := a
-
 check @id
 
 inductive list :=