diff --git a/tests/lean/bad_coercions.lean b/tests/lean/bad_coercions.lean index d8830bfbd..2d54b684b 100644 --- a/tests/lean/bad_coercions.lean +++ b/tests/lean/bad_coercions.lean @@ -1,4 +1,3 @@ -import data.nat.basic open nat constant list.{l} : Type.{l} → Type.{l} diff --git a/tests/lean/bad_coercions.lean.expected.out b/tests/lean/bad_coercions.lean.expected.out index 70f7526b9..de72b0560 100644 --- a/tests/lean/bad_coercions.lean.expected.out +++ b/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:19:11: error: invalid 'coercion' command, coercions cannot be defined in contexts +bad_coercions.lean:12:18: error: invalid '[coercion]' modifier, coercions cannot be defined in contexts +bad_coercions.lean:18:11: error: invalid 'coercion' command, coercions cannot be defined in contexts diff --git a/tests/lean/bad_notation.lean b/tests/lean/bad_notation.lean index acb2ed317..eff773aff 100644 --- a/tests/lean/bad_notation.lean +++ b/tests/lean/bad_notation.lean @@ -1,4 +1,4 @@ -import logic data.nat.basic +import logic open nat section diff --git a/tests/lean/error_full_names.lean b/tests/lean/error_full_names.lean index 77ea01652..f3e13c23c 100644 --- a/tests/lean/error_full_names.lean +++ b/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 diff --git a/tests/lean/error_full_names.lean.expected.out b/tests/lean/error_full_names.lean.expected.out index e592afff1..81bb5d2d1 100644 --- a/tests/lean/error_full_names.lean.expected.out +++ b/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 diff --git a/tests/lean/ftree.lean b/tests/lean/ftree.lean index e4fb30acb..8d6264871 100644 --- a/tests/lean/ftree.lean +++ b/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 diff --git a/tests/lean/inv_del.lean b/tests/lean/inv_del.lean index 3c6c036fb..4cfca0bce 100644 --- a/tests/lean/inv_del.lean +++ b/tests/lean/inv_del.lean @@ -1,4 +1,4 @@ -import logic data.nat.basic +import logic open nat inductive vec (A : Type) : nat → Type := diff --git a/tests/lean/namespace_bug.lean b/tests/lean/namespace_bug.lean index 0f6d20f68..32059d1fe 100644 --- a/tests/lean/namespace_bug.lean +++ b/tests/lean/namespace_bug.lean @@ -1,5 +1,3 @@ -import data.nat.basic - namespace playground namespace nat check 2+3 -- Should produce error diff --git a/tests/lean/namespace_bug.lean.expected.out b/tests/lean/namespace_bug.lean.expected.out index 41af89829..3a51b03f0 100644 --- a/tests/lean/namespace_bug.lean.expected.out +++ b/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 diff --git a/tests/lean/no_confusion_type.lean b/tests/lean/no_confusion_type.lean index aedb43127..3087f4624 100644 --- a/tests/lean/no_confusion_type.lean +++ b/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 := diff --git a/tests/lean/notation.lean b/tests/lean/notation.lean index e8789e886..d68eeb1db 100644 --- a/tests/lean/notation.lean +++ b/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 diff --git a/tests/lean/notation2.lean b/tests/lean/notation2.lean index 306011cd2..25372a356 100644 --- a/tests/lean/notation2.lean +++ b/tests/lean/notation2.lean @@ -1,5 +1,5 @@ -import data.list data.num -open list +import data.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 infixr `::` := cons check 1 :: 2 :: nil check 1 :: 2 :: 3 :: 4 :: 5 :: nil diff --git a/tests/lean/notation3.lean b/tests/lean/notation3.lean index c806bd76d..6e82b417c 100644 --- a/tests/lean/notation3.lean +++ b/tests/lean/notation3.lean @@ -1,5 +1,6 @@ -import data.prod data.list data.num -open list prod num +import data.prod data.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) diff --git a/tests/lean/notation4.lean b/tests/lean/notation4.lean index e5bf751c2..5f63b2ee6 100644 --- a/tests/lean/notation4.lean +++ 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 diff --git a/tests/lean/print_ax1.lean b/tests/lean/print_ax1.lean index 7e3deeadc..912e0dbde 100644 --- a/tests/lean/print_ax1.lean +++ b/tests/lean/print_ax1.lean @@ -1,3 +1 @@ -import data.nat.basic - print axioms diff --git a/tests/lean/proj.lean b/tests/lean/proj.lean index 1fcd06a86..5ab3f8ebd 100644 --- a/tests/lean/proj.lean +++ b/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, diff --git a/tests/lean/tuple.lean b/tests/lean/tuple.lean index a6e792547..6cffe335c 100644 --- a/tests/lean/tuple.lean +++ b/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 diff --git a/tests/lean/uni_bug1.lean b/tests/lean/uni_bug1.lean index 11151b014..e54fc08c1 100644 --- a/tests/lean/uni_bug1.lean +++ b/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 diff --git a/tests/lean/whnf.lean b/tests/lean/whnf.lean index 4446958da..e6405e730 100644 --- a/tests/lean/whnf.lean +++ b/tests/lean/whnf.lean @@ -1,4 +1,3 @@ -import data.nat.basic open nat eval [whnf] (fun x, x + 1) 2