test(tests/lean): remove data.nat dependency

tests/lean/bad_coercions.lean

@@ -1,4 +1,3 @@
-import data.nat.basic
 open nat
 
 constant list.{l} : Type.{l} → Type.{l}

tests/lean/bad_coercions.lean.expected.out

@@ -1,2 +1,2 @@
-bad_coercions.lean:13:18: error: invalid '[coercion]' modifier, coercions cannot be defined in contexts
+bad_coercions.lean:12:18: error: invalid '[coercion]' modifier, coercions cannot be defined in contexts
-bad_coercions.lean:19:11: error: invalid 'coercion' command, coercions cannot be defined in contexts
+bad_coercions.lean:18:11: error: invalid 'coercion' command, coercions cannot be defined in contexts

tests/lean/bad_notation.lean

@@ -1,4 +1,4 @@
-import logic data.nat.basic
+import logic
 open nat
 
 section

tests/lean/error_full_names.lean

@@ -1,4 +1,3 @@
-import data.nat.basic
 namespace foo
 open nat
 inductive nat : Type := zero, foosucc : nat → nat

tests/lean/error_full_names.lean.expected.out

@@ -1,4 +1,4 @@
-error_full_names.lean:5:8: error: type mismatch at application
+error_full_names.lean:4:8: error: type mismatch at application
   0 + nat.zero
 term
   nat.zero
@@ -6,7 +6,7 @@ has type
   nat
 but is expected to have type
   ℕ
-error_full_names.lean:9:6: error: type mismatch at application
+error_full_names.lean:8:6: error: type mismatch at application
   nat.succ nat.zero
 term
   nat.zero

tests/lean/ftree.lean

@@ -1,4 +1,4 @@
-import data.list
+inductive list (T : Type) : Type := nil {} : list T, cons   : T → list T → list T
 
 namespace explicit
 

tests/lean/inv_del.lean

@@ -1,4 +1,4 @@
-import logic data.nat.basic
+import logic
 open nat
 
 inductive vec (A : Type) : nat → Type :=

tests/lean/namespace_bug.lean

@@ -1,5 +1,3 @@
-import data.nat.basic
-
 namespace playground
 namespace nat
 check 2+3 -- Should produce error

tests/lean/namespace_bug.lean.expected.out

@@ -1 +1 @@
-namespace_bug.lean:5:7: error: invalid expression
+namespace_bug.lean:3:7: error: invalid expression

tests/lean/no_confusion_type.lean

@@ -1,4 +1,4 @@
-import logic data.nat.basic
+import logic
 open nat
 
 inductive vector (A : Type) : nat → Type :=

tests/lean/notation.lean

@@ -1,4 +1,4 @@
-import logic data.num data.nat.basic
+import logic data.num
 open num
 constant b : num
 check b + b + b

tests/lean/notation2.lean

@@ -1,5 +1,5 @@
-import data.list data.num
+import data.num
-open list
+inductive list (T : Type) : Type := nil {} : list T, cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 infixr `::` := cons
 check 1 :: 2 :: nil
 check 1 :: 2 :: 3 :: 4 :: 5 :: nil

tests/lean/notation3.lean

@@ -1,5 +1,6 @@
-import data.prod data.list data.num
+import data.prod data.num
-open list prod num
+inductive list (T : Type) : Type := nil {} : list T, cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
+open prod num
 constants a b : num
 check [a, b, b]
 check (a, true, a = b, b)

tests/lean/notation4.lean

@@ -1,6 +1,6 @@
-import logic data.sigma data.list
+import logic data.sigma
 open sigma
-
+inductive list (T : Type) : Type := nil {} : list T, cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 check ∃ (A : Type₁) (x y : A), x = y
 check ∃ (x : num), x = 0
 check Σ (x : num), x = 10

tests/lean/print_ax1.lean

@@ -1,3 +1 @@
-import data.nat.basic
-
 print axioms

tests/lean/proj.lean

@@ -1,4 +1,4 @@
-import logic data.nat.basic
+import logic
 
 inductive vector (T : Type) : nat → Type :=
   nil {} : vector T nat.zero,

tests/lean/tuple.lean

@@ -1,4 +1,4 @@
-import data.nat.basic data.prod
+import data.prod
 open nat prod
 
 set_option pp.universes true

tests/lean/uni_bug1.lean

@@ -1,4 +1,4 @@
-import data.nat.basic data.prod
+import data.prod
 open nat prod
 
 constant R : nat → nat → Prop

tests/lean/whnf.lean

@@ -1,4 +1,3 @@
-import data.nat.basic
 open nat
 
 eval [whnf] (fun x, x + 1) 2