diff --git a/tests/lean/record_rec_protected.lean b/tests/lean/record_rec_protected.lean index a84cdf02bb..c6e6e2d25b 100644 --- a/tests/lean/record_rec_protected.lean +++ b/tests/lean/record_rec_protected.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic structure point (A : Type) (B : Type) := mk :: (x : A) (y : B) diff --git a/tests/lean/run/coe6.lean b/tests/lean/run/coe6.lean index 1247197ce2..cabd3444eb 100644 --- a/tests/lean/run/coe6.lean +++ b/tests/lean/run/coe6.lean @@ -1,4 +1,4 @@ -import data.unit +-- import data.unit open unit namespace play constant int : Type.{1} diff --git a/tests/lean/run/confuse_ind.lean b/tests/lean/run/confuse_ind.lean index cad894350c..123e818091 100644 --- a/tests/lean/run/confuse_ind.lean +++ b/tests/lean/run/confuse_ind.lean @@ -1,4 +1,4 @@ -import logic data.prod data.unit +import logic data.prod definition mk_arrow (A : Type) (B : Type) := A → A → B diff --git a/tests/lean/run/decidable.lean b/tests/lean/run/decidable.lean index 7d712e29cd..a4f459ec53 100644 --- a/tests/lean/run/decidable.lean +++ b/tests/lean/run/decidable.lean @@ -1,4 +1,4 @@ -import logic data.unit data.bool +import logic data.bool open bool unit decidable constants a b c : bool diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean index 6678100720..087e911945 100644 --- a/tests/lean/run/group3.lean +++ b/tests/lean/run/group3.lean @@ -8,7 +8,7 @@ -- Various structures with 1, *, inv, including groups. import logic.eq -import data.unit data.sigma data.prod +import data.sigma data.prod import algebra.binary open eq diff --git a/tests/lean/run/record1.lean b/tests/lean/run/record1.lean index e8d60eedd2..e99f2f8f1f 100644 --- a/tests/lean/run/record1.lean +++ b/tests/lean/run/record1.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic structure point (A : Type) (B : Type) := diff --git a/tests/lean/run/record2.lean b/tests/lean/run/record2.lean index 34a47978d9..e2a4ee483b 100644 --- a/tests/lean/run/record2.lean +++ b/tests/lean/run/record2.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic set_option pp.universes true diff --git a/tests/lean/run/record3.lean b/tests/lean/run/record3.lean index 2ffb31875d..0c8de6cdb3 100644 --- a/tests/lean/run/record3.lean +++ b/tests/lean/run/record3.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic structure point (A : Type) (B : Type) := diff --git a/tests/lean/run/record4.lean b/tests/lean/run/record4.lean index 93b5f2f600..aa9433f689 100644 --- a/tests/lean/run/record4.lean +++ b/tests/lean/run/record4.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic set_option structure.eta_thm true diff --git a/tests/lean/run/record5.lean b/tests/lean/run/record5.lean index 6811a22325..76e706a574 100644 --- a/tests/lean/run/record5.lean +++ b/tests/lean/run/record5.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic structure point (A : Type) (B : Type) := mk :: (x : A) (y : B) diff --git a/tests/lean/run/record6.lean b/tests/lean/run/record6.lean index 902cbab985..77e4f59659 100644 --- a/tests/lean/run/record6.lean +++ b/tests/lean/run/record6.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic structure point (A : Type) (B : Type) := mk :: (x : A) (y : B) diff --git a/tests/lean/run/record7.lean b/tests/lean/run/record7.lean index 60031b31e0..c9794f87ae 100644 --- a/tests/lean/run/record7.lean +++ b/tests/lean/run/record7.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic structure point (A : Type) (B : Type) := mk :: (x : A) (y : B)