From 0e8838df3b63aa471e24e1c7e19b7a7d72f0b1c7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Aug 2025 14:04:42 +0200 Subject: [PATCH] chore: avoid confusing `public import all` combination (#10051) --- src/Init/Control/Lawful/Instances.lean | 6 ++- .../Control/Lawful/MonadLift/Instances.lean | 18 ++++++--- src/Init/Data/Array/Attach.lean | 3 +- src/Init/Data/Array/Basic.lean | 6 ++- src/Init/Data/Array/BasicAux.lean | 3 +- src/Init/Data/Array/Bootstrap.lean | 3 +- src/Init/Data/Array/Count.lean | 3 +- src/Init/Data/Array/DecidableEq.lean | 3 +- src/Init/Data/Array/Erase.lean | 3 +- src/Init/Data/Array/Find.lean | 3 +- src/Init/Data/Array/MapIdx.lean | 6 ++- src/Init/Data/Array/Monadic.lean | 6 ++- src/Init/Data/Array/OfFn.lean | 3 +- src/Init/Data/Array/Perm.lean | 3 +- src/Init/Data/Array/Range.lean | 6 ++- src/Init/Data/Array/Subarray/Split.lean | 3 +- src/Init/Data/Array/TakeDrop.lean | 3 +- src/Init/Data/Array/Zip.lean | 3 +- src/Init/Data/BitVec/Bitblast.lean | 9 +++-- src/Init/Data/BitVec/Bootstrap.lean | 3 +- src/Init/Data/BitVec/Folds.lean | 3 +- src/Init/Data/BitVec/Lemmas.lean | 6 ++- src/Init/Data/ByteArray/Basic.lean | 3 +- src/Init/Data/Char/Lemmas.lean | 3 +- src/Init/Data/Int/Bitwise/Lemmas.lean | 3 +- src/Init/Data/Int/Compare.lean | 3 +- src/Init/Data/Int/Linear.lean | 6 ++- .../Iterators/Lemmas/Combinators/Attach.lean | 6 ++- .../Lemmas/Combinators/Monadic/Attach.lean | 3 +- .../Lemmas/Combinators/Monadic/FilterMap.lean | 3 +- .../Lemmas/Combinators/Monadic/ULift.lean | 3 +- .../Iterators/Lemmas/Combinators/ULift.lean | 3 +- .../Iterators/Lemmas/Consumers/Collect.lean | 6 ++- .../Data/Iterators/Lemmas/Consumers/Loop.lean | 9 +++-- .../Lemmas/Consumers/Monadic/Collect.lean | 3 +- .../Lemmas/Consumers/Monadic/Loop.lean | 3 +- src/Init/Data/List/Attach.lean | 3 +- src/Init/Data/List/FinRange.lean | 3 +- src/Init/Data/List/Find.lean | 3 +- src/Init/Data/List/Lemmas.lean | 6 ++- src/Init/Data/List/Monadic.lean | 3 +- src/Init/Data/List/Perm.lean | 3 +- src/Init/Data/List/Sort/Impl.lean | 3 +- src/Init/Data/List/Sort/Lemmas.lean | 3 +- src/Init/Data/List/TakeDrop.lean | 3 +- src/Init/Data/List/ToArray.lean | 9 +++-- src/Init/Data/Nat/Bitwise/Lemmas.lean | 3 +- src/Init/Data/Nat/Compare.lean | 3 +- src/Init/Data/Nat/Lemmas.lean | 6 ++- src/Init/Data/Option/Array.lean | 3 +- src/Init/Data/Option/Lemmas.lean | 6 ++- src/Init/Data/Option/List.lean | 6 ++- src/Init/Data/Option/Monadic.lean | 3 +- src/Init/Data/Ord/Basic.lean | 3 +- src/Init/Data/Range/Lemmas.lean | 3 +- src/Init/Data/Range/Polymorphic/Lemmas.lean | 12 ++++-- src/Init/Data/SInt/Bitwise.lean | 12 ++++-- src/Init/Data/SInt/Lemmas.lean | 12 ++++-- src/Init/Data/Slice/Array/Iterator.lean | 3 +- src/Init/Data/Slice/Array/Lemmas.lean | 15 +++++--- src/Init/Data/Slice/Lemmas.lean | 3 +- src/Init/Data/String/Extra.lean | 6 ++- src/Init/Data/Sum/Lemmas.lean | 3 +- src/Init/Data/UInt/Bitwise.lean | 6 ++- src/Init/Data/UInt/Lemmas.lean | 15 +++++--- src/Init/Data/Vector/Attach.lean | 3 +- src/Init/Data/Vector/Count.lean | 6 ++- src/Init/Data/Vector/Find.lean | 6 ++- src/Init/Data/Vector/Lemmas.lean | 6 ++- src/Init/Data/Vector/Lex.lean | 6 ++- src/Init/Data/Vector/MapIdx.lean | 6 ++- src/Init/Data/Vector/Monadic.lean | 3 +- src/Init/Data/Vector/OfFn.lean | 3 +- src/Init/Data/Vector/Perm.lean | 6 ++- src/Init/Data/Vector/Range.lean | 6 ++- src/Init/Data/Vector/Zip.lean | 6 ++- src/Init/Grind/Module/Basic.lean | 3 +- src/Init/Grind/Module/Envelope.lean | 3 +- src/Init/Grind/Ordered/Linarith.lean | 6 ++- src/Init/Grind/Ring/Envelope.lean | 3 +- src/Init/Grind/Ring/Poly.lean | 3 +- src/Init/Grind/ToIntLemmas.lean | 3 +- src/Init/GrindInstances/Ring/BitVec.lean | 6 ++- src/Init/GrindInstances/Ring/Fin.lean | 6 ++- src/Init/GrindInstances/Ring/SInt.lean | 9 +++-- src/Init/GrindInstances/Ring/UInt.lean | 6 ++- src/Init/GrindInstances/ToInt.lean | 3 +- src/Init/Internal/Order/Basic.lean | 3 +- src/Init/Internal/Order/Lemmas.lean | 9 +++-- src/Init/Meta.lean | 3 +- src/Init/Omega/Coeffs.lean | 3 +- src/Init/SizeOfLemmas.lean | 6 ++- src/Lean/Parser/Module.lean | 38 +++++++++++-------- src/Std/Data/DHashMap/Basic.lean | 3 +- .../DHashMap/Internal/AssocList/Lemmas.lean | 3 +- src/Std/Data/DHashMap/Internal/Model.lean | 3 +- src/Std/Data/DHashMap/Internal/Raw.lean | 3 +- src/Std/Data/DHashMap/Lemmas.lean | 3 +- src/Std/Data/DHashMap/RawLemmas.lean | 3 +- src/Std/Data/Internal/List/Associative.lean | 3 +- .../Iterators/Lemmas/Producers/Slice.lean | 3 +- src/Std/Time/Date/ValidDate.lean | 3 +- src/Std/Time/Format.lean | 3 +- tests/lean/moduleKeywords.lean.expected.out | 6 +-- tests/pkg/module/Module/ImportedAll.lean | 3 +- .../Module/ImportedAllPrivateImported.lean | 3 +- 106 files changed, 354 insertions(+), 182 deletions(-) diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean index df8fc13403..c9b5773dde 100644 --- a/src/Init/Control/Lawful/Instances.lean +++ b/src/Init/Control/Lawful/Instances.lean @@ -7,8 +7,10 @@ module prelude public import Init.Control.Lawful.Basic -public import all Init.Control.Except -public import all Init.Control.State +public import Init.Control.Except +import all Init.Control.Except +public import Init.Control.State +import all Init.Control.State public import Init.Control.StateRef public import Init.Ext diff --git a/src/Init/Control/Lawful/MonadLift/Instances.lean b/src/Init/Control/Lawful/MonadLift/Instances.lean index 79a38d8251..7321efe9ad 100644 --- a/src/Init/Control/Lawful/MonadLift/Instances.lean +++ b/src/Init/Control/Lawful/MonadLift/Instances.lean @@ -6,12 +6,18 @@ Authors: Quang Dao, Paul Reichert module prelude -public import all Init.Control.Option -public import all Init.Control.Except -public import all Init.Control.ExceptCps -public import all Init.Control.StateRef -public import all Init.Control.StateCps -public import all Init.Control.Id +public import Init.Control.Option +import all Init.Control.Option +public import Init.Control.Except +import all Init.Control.Except +public import Init.Control.ExceptCps +import all Init.Control.ExceptCps +public import Init.Control.StateRef +import all Init.Control.StateRef +public import Init.Control.StateCps +import all Init.Control.StateCps +public import Init.Control.Id +import all Init.Control.Id public import Init.Control.Lawful.MonadLift.Lemmas public import Init.Control.Lawful.Instances diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean index a79c2a9cf2..142064408a 100644 --- a/src/Init/Data/Array/Attach.lean +++ b/src/Init/Data/Array/Attach.lean @@ -9,7 +9,8 @@ prelude public import Init.Data.Array.Mem public import Init.Data.Array.Lemmas public import Init.Data.Array.Count -public import all Init.Data.List.Attach +public import Init.Data.List.Attach +import all Init.Data.List.Attach public section diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 3d759f832a..805768ff9d 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -13,8 +13,10 @@ public import Init.Data.UInt.BasicAux public import Init.Data.Repr public import Init.Data.ToString.Basic public import Init.GetElem -public import all Init.Data.List.ToArrayImpl -public import all Init.Data.Array.Set +public import Init.Data.List.ToArrayImpl +import all Init.Data.List.ToArrayImpl +public import Init.Data.Array.Set +import all Init.Data.Array.Set public section diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean index 6c96cdaddd..8a335ff236 100644 --- a/src/Init/Data/Array/BasicAux.lean +++ b/src/Init/Data/Array/BasicAux.lean @@ -6,7 +6,8 @@ Authors: Leonardo de Moura module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Nat.Linear public import Init.NotationExtra diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index 8c49b46fbe..23752e43e9 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -8,7 +8,8 @@ module prelude public import Init.Data.List.TakeDrop -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public section diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean index 5d1b61a93e..10e0431629 100644 --- a/src/Init/Data/Array/Count.lean +++ b/src/Init/Data/Array/Count.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Lemmas public import Init.Data.List.Nat.Count diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index fd96598073..595743b1b0 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -6,7 +6,8 @@ Authors: Leonardo de Moura module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.BEq public import Init.Data.List.Nat.BEq public import Init.ByCases diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean index ac63111e38..5052e310bd 100644 --- a/src/Init/Data/Array/Erase.lean +++ b/src/Init/Data/Array/Erase.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Lemmas public import Init.Data.List.Nat.Erase public import Init.Data.List.Nat.Basic diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index 775aabb0e1..f9081325d9 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean @@ -7,7 +7,8 @@ module prelude public import Init.Data.List.Nat.Find -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Lemmas public import Init.Data.Array.Attach public import Init.Data.Array.Range diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index ee6150a800..b27ba6a328 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -6,11 +6,13 @@ Authors: Mario Carneiro, Kim Morrison module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Lemmas public import Init.Data.Array.Attach public import Init.Data.Array.OfFn -public import all Init.Data.List.MapIdx +public import Init.Data.List.MapIdx +import all Init.Data.List.MapIdx public section diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean index e8e8c25e81..614629bcb4 100644 --- a/src/Init/Data/Array/Monadic.lean +++ b/src/Init/Data/Array/Monadic.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -public import all Init.Data.List.Control -public import all Init.Data.Array.Basic +public import Init.Data.List.Control +import all Init.Data.List.Control +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Lemmas public import Init.Data.Array.Attach public import Init.Data.List.Monadic diff --git a/src/Init/Data/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean index 8d8238b9a2..4445c048e8 100644 --- a/src/Init/Data/Array/OfFn.lean +++ b/src/Init/Data/Array/OfFn.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Lemmas public import Init.Data.Array.Monadic public import Init.Data.List.OfFn diff --git a/src/Init/Data/Array/Perm.lean b/src/Init/Data/Array/Perm.lean index 9e8a4d922b..d876a6f2fb 100644 --- a/src/Init/Data/Array/Perm.lean +++ b/src/Init/Data/Array/Perm.lean @@ -7,7 +7,8 @@ module prelude public import Init.Data.List.Nat.Perm -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Lemmas public section diff --git a/src/Init/Data/Array/Range.lean b/src/Init/Data/Array/Range.lean index 16b05f1400..b6ea55ad39 100644 --- a/src/Init/Data/Array/Range.lean +++ b/src/Init/Data/Array/Range.lean @@ -7,8 +7,10 @@ module prelude public import Init.Data.Array.Lemmas -public import all Init.Data.Array.Basic -public import all Init.Data.Array.OfFn +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic +public import Init.Data.Array.OfFn +import all Init.Data.Array.OfFn public import Init.Data.Array.MapIdx public import Init.Data.Array.Zip public import Init.Data.List.Nat.Range diff --git a/src/Init/Data/Array/Subarray/Split.lean b/src/Init/Data/Array/Subarray/Split.lean index 61cd40dd65..96b2c78c5b 100644 --- a/src/Init/Data/Array/Subarray/Split.lean +++ b/src/Init/Data/Array/Subarray/Split.lean @@ -8,7 +8,8 @@ module prelude public import Init.Data.Array.Basic -public import all Init.Data.Array.Subarray +public import Init.Data.Array.Subarray +import all Init.Data.Array.Subarray public import Init.Omega public section diff --git a/src/Init/Data/Array/TakeDrop.lean b/src/Init/Data/Array/TakeDrop.lean index 805d7d9dd7..b2af1864ff 100644 --- a/src/Init/Data/Array/TakeDrop.lean +++ b/src/Init/Data/Array/TakeDrop.lean @@ -6,7 +6,8 @@ Authors: Markus Himmel module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Lemmas public import Init.Data.List.Nat.TakeDrop diff --git a/src/Init/Data/Array/Zip.lean b/src/Init/Data/Array/Zip.lean index 92c1b82196..d24abfbc6e 100644 --- a/src/Init/Data/Array/Zip.lean +++ b/src/Init/Data/Array/Zip.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.TakeDrop public import Init.Data.List.Zip diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index a1b4d8a103..0925dc9e97 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -6,11 +6,14 @@ Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat module prelude -public import all Init.Data.Nat.Bitwise.Basic +public import Init.Data.Nat.Bitwise.Basic +import all Init.Data.Nat.Bitwise.Basic public import Init.Data.Nat.Mod -public import all Init.Data.Int.DivMod +public import Init.Data.Int.DivMod +import all Init.Data.Int.DivMod public import Init.Data.Int.LemmasAux -public import all Init.Data.BitVec.Basic +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic public import Init.Data.BitVec.Decidable public import Init.Data.BitVec.Lemmas public import Init.Data.BitVec.Folds diff --git a/src/Init/Data/BitVec/Bootstrap.lean b/src/Init/Data/BitVec/Bootstrap.lean index 44ba6bfe42..287c1599dd 100644 --- a/src/Init/Data/BitVec/Bootstrap.lean +++ b/src/Init/Data/BitVec/Bootstrap.lean @@ -6,7 +6,8 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B module prelude -public import all Init.Data.BitVec.Basic +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic public section diff --git a/src/Init/Data/BitVec/Folds.lean b/src/Init/Data/BitVec/Folds.lean index 39d4d53914..8fee9547ed 100644 --- a/src/Init/Data/BitVec/Folds.lean +++ b/src/Init/Data/BitVec/Folds.lean @@ -6,7 +6,8 @@ Authors: Joe Hendrix, Harun Khan module prelude -public import all Init.Data.BitVec.Basic +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic public import Init.Data.BitVec.Lemmas public import Init.Data.Nat.Lemmas public import Init.Data.Fin.Iterate diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index d0b75e50d9..1f98f03474 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -7,8 +7,10 @@ module prelude public import Init.Data.Bool -public import all Init.Data.BitVec.Basic -public import all Init.Data.BitVec.BasicAux +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic +public import Init.Data.BitVec.BasicAux +import all Init.Data.BitVec.BasicAux public import Init.Data.Fin.Lemmas public import Init.Data.Nat.Lemmas public import Init.Data.Nat.Div.Lemmas diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 5f72952e83..d74037e5e9 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -9,7 +9,8 @@ prelude public import Init.Data.Array.Basic public import Init.Data.Array.DecidableEq public import Init.Data.UInt.Basic -public import all Init.Data.UInt.BasicAux +public import Init.Data.UInt.BasicAux +import all Init.Data.UInt.BasicAux public import Init.Data.Option.Basic @[expose] public section diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean index 09e7ae6f59..a127b5c6f5 100644 --- a/src/Init/Data/Char/Lemmas.lean +++ b/src/Init/Data/Char/Lemmas.lean @@ -6,7 +6,8 @@ Authors: Leonardo de Moura module prelude -public import all Init.Data.Char.Basic +public import Init.Data.Char.Basic +import all Init.Data.Char.Basic public import Init.Data.UInt.Lemmas public section diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index ae3b94a351..03f38e79e9 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -7,7 +7,8 @@ module prelude public import Init.Data.Nat.Bitwise.Lemmas -public import all Init.Data.Int.Bitwise.Basic +public import Init.Data.Int.Bitwise.Basic +import all Init.Data.Int.Bitwise.Basic public import Init.Data.Int.DivMod.Lemmas public section diff --git a/src/Init/Data/Int/Compare.lean b/src/Init/Data/Int/Compare.lean index d10d35b2e8..add211cc2c 100644 --- a/src/Init/Data/Int/Compare.lean +++ b/src/Init/Data/Int/Compare.lean @@ -6,7 +6,8 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert module prelude -public import all Init.Data.Ord.Basic +public import Init.Data.Ord.Basic +import all Init.Data.Ord.Basic public import Init.Data.Int.Order public section diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index aca2c7fd40..8ccb80d868 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/src/Init/Data/Int/Linear.lean @@ -12,9 +12,11 @@ public import Init.Data.Int.Lemmas public import Init.Data.Int.LemmasAux public import Init.Data.Int.DivMod.Bootstrap public import Init.Data.Int.Cooper -public import all Init.Data.Int.Gcd +public import Init.Data.Int.Gcd +import all Init.Data.Int.Gcd public import Init.Data.RArray -public import all Init.Data.AC +public import Init.Data.AC +import all Init.Data.AC public section diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean index 73081d60e9..13c9fa258c 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -public import all Init.Data.Iterators.Combinators.Attach -public import all Init.Data.Iterators.Combinators.Monadic.Attach +public import Init.Data.Iterators.Combinators.Attach +import all Init.Data.Iterators.Combinators.Attach +public import Init.Data.Iterators.Combinators.Monadic.Attach +import all Init.Data.Iterators.Combinators.Monadic.Attach public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach public import Init.Data.Iterators.Lemmas.Consumers.Collect public import Init.Data.Array.Attach diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean index 11b7335b13..071de3052f 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean @@ -6,7 +6,8 @@ Authors: Paul Reichert module prelude -public import all Init.Data.Iterators.Combinators.Monadic.Attach +public import Init.Data.Iterators.Combinators.Monadic.Attach +import all Init.Data.Iterators.Combinators.Monadic.Attach public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect public section diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean index e63f23593b..8a1562b89e 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean @@ -9,7 +9,8 @@ prelude public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction public import Init.Data.Iterators.Combinators.Monadic.FilterMap public import Init.Data.Iterators.Lemmas.Consumers.Monadic -public import all Init.Data.Iterators.Consumers.Monadic.Collect +public import Init.Data.Iterators.Consumers.Monadic.Collect +import all Init.Data.Iterators.Consumers.Monadic.Collect public section diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean index c4f3f02902..f6d6a71d60 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean @@ -6,7 +6,8 @@ Authors: Paul Reichert module prelude -public import all Init.Data.Iterators.Combinators.Monadic.ULift +public import Init.Data.Iterators.Combinators.Monadic.ULift +import all Init.Data.Iterators.Combinators.Monadic.ULift public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect public section diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean index 5589910906..d504f55c86 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean @@ -6,7 +6,8 @@ Authors: Paul Reichert module prelude -public import all Init.Data.Iterators.Combinators.ULift +public import Init.Data.Iterators.Combinators.ULift +import all Init.Data.Iterators.Combinators.ULift public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift public import Init.Data.Iterators.Lemmas.Consumers.Collect diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean index c7369f57bd..95490ec822 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean @@ -8,8 +8,10 @@ module prelude public import Init.Data.Iterators.Lemmas.Basic public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect -public import all Init.Data.Iterators.Consumers.Access -public import all Init.Data.Iterators.Consumers.Collect +public import Init.Data.Iterators.Consumers.Access +import all Init.Data.Iterators.Consumers.Access +public import Init.Data.Iterators.Consumers.Collect +import all Init.Data.Iterators.Consumers.Collect public section diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index 0be561a3bd..b6e289d8bc 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -8,9 +8,12 @@ module prelude public import Init.Control.Lawful.MonadLift.Instances public import Init.Data.Iterators.Lemmas.Consumers.Collect -public import all Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop -public import all Init.Data.Iterators.Consumers.Loop -public import all Init.Data.Iterators.Consumers.Monadic.Collect +public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop +import all Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop +public import Init.Data.Iterators.Consumers.Loop +import all Init.Data.Iterators.Consumers.Loop +public import Init.Data.Iterators.Consumers.Monadic.Collect +import all Init.Data.Iterators.Consumers.Monadic.Collect public section diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean index 87680df70c..87e5445400 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean @@ -8,7 +8,8 @@ module prelude public import Init.Data.Array.Lemmas public import Init.Data.Iterators.Lemmas.Monadic.Basic -public import all Init.Data.Iterators.Consumers.Monadic.Collect +public import Init.Data.Iterators.Consumers.Monadic.Collect +import all Init.Data.Iterators.Consumers.Monadic.Collect public section diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean index 597f7cf373..370b8442ce 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean @@ -7,7 +7,8 @@ module prelude public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect -public import all Init.Data.Iterators.Consumers.Monadic.Loop +public import Init.Data.Iterators.Consumers.Monadic.Loop +import all Init.Data.Iterators.Consumers.Monadic.Loop public section diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 567c5ed82b..4b716c6663 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -6,7 +6,8 @@ Authors: Mario Carneiro module prelude -public import all Init.Data.List.Lemmas -- for dsimping with `getElem?_cons_succ` +public import Init.Data.List.Lemmas -- for dsimping with `getElem?_cons_succ` +import all Init.Data.List.Lemmas -- for dsimping with `getElem?_cons_succ` public import Init.Data.List.Count public import Init.Data.Subtype.Basic public import Init.BinderNameHint diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean index 97a56a8168..99c205c6c2 100644 --- a/src/Init/Data/List/FinRange.lean +++ b/src/Init/Data/List/FinRange.lean @@ -6,7 +6,8 @@ Authors: François G. Dorais module prelude -public import all Init.Data.List.OfFn +public import Init.Data.List.OfFn +import all Init.Data.List.OfFn public import Init.Data.List.Monadic public section diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index cb8f55f463..213d108be3 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -11,7 +11,8 @@ public import Init.Data.List.Lemmas public import Init.Data.List.Sublist public import Init.Data.List.Range public import Init.Data.List.Impl -public import all Init.Data.List.Attach +public import Init.Data.List.Attach +import all Init.Data.List.Attach public import Init.Data.Fin.Lemmas public section diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 76be4f57b1..db00d2defd 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -9,8 +9,10 @@ module prelude public import Init.Data.Bool public import Init.Data.Option.Lemmas -public import all Init.Data.List.BasicAux -public import all Init.Data.List.Control +public import Init.Data.List.BasicAux +import all Init.Data.List.BasicAux +public import Init.Data.List.Control +import all Init.Data.List.Control public import Init.Control.Lawful.Basic public import Init.BinderPredicates diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean index 4a2579c560..60659157ac 100644 --- a/src/Init/Data/List/Monadic.lean +++ b/src/Init/Data/List/Monadic.lean @@ -10,7 +10,8 @@ public import Init.Data.List.TakeDrop public import Init.Data.List.Attach public import Init.Data.List.OfFn public import Init.Data.Array.Bootstrap -public import all Init.Data.List.Control +public import Init.Data.List.Control +import all Init.Data.List.Control public section diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean index 23eb6848a0..40c3ac560d 100644 --- a/src/Init/Data/List/Perm.lean +++ b/src/Init/Data/List/Perm.lean @@ -9,7 +9,8 @@ prelude public import Init.Data.List.Pairwise public import Init.Data.List.Erase public import Init.Data.List.Find -public import all Init.Data.List.Attach +public import Init.Data.List.Attach +import all Init.Data.List.Attach public section diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean index 0533a079d9..df4df966c2 100644 --- a/src/Init/Data/List/Sort/Impl.lean +++ b/src/Init/Data/List/Sort/Impl.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Data.List.Sort.Basic +public import Init.Data.List.Sort.Basic +import all Init.Data.List.Sort.Basic public import Init.Data.List.Sort.Lemmas public section diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index 05f1f4e154..94547554ce 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -7,7 +7,8 @@ module prelude public import Init.Data.List.Perm -public import all Init.Data.List.Sort.Basic +public import Init.Data.List.Sort.Basic +import all Init.Data.List.Sort.Basic public import Init.Data.List.Nat.Range public import Init.Data.Bool diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 8647777032..6ad2dcbd63 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -6,7 +6,8 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -public import all Init.Data.List.Basic +public import Init.Data.List.Basic +import all Init.Data.List.Basic public import Init.Data.List.Lemmas public section diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 843ce04bdb..7de1c968eb 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -6,14 +6,17 @@ Authors: Mario Carneiro module prelude -public import all Init.Data.List.Control +public import Init.Data.List.Control +import all Init.Data.List.Control public import Init.Data.List.Impl public import Init.Data.List.Nat.Erase public import Init.Data.List.Monadic public import Init.Data.List.Nat.InsertIdx public import Init.Data.Array.Lex.Basic -public import all Init.Data.Array.Basic -public import all Init.Data.Array.Set +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic +public import Init.Data.Array.Set +import all Init.Data.Array.Set public section diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index 8fcd299c6e..c0d1e78e3a 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -9,7 +9,8 @@ module prelude public import Init.Data.Bool public import Init.Data.Int.Pow -public import all Init.Data.Nat.Bitwise.Basic +public import Init.Data.Nat.Bitwise.Basic +import all Init.Data.Nat.Bitwise.Basic public import Init.Data.Nat.Lemmas public import Init.Data.Nat.Simproc public import Init.TacticsExtra diff --git a/src/Init/Data/Nat/Compare.lean b/src/Init/Data/Nat/Compare.lean index 9239fae0fe..de6c6d8d3e 100644 --- a/src/Init/Data/Nat/Compare.lean +++ b/src/Init/Data/Nat/Compare.lean @@ -6,7 +6,8 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro module prelude -public import all Init.Data.Ord.Basic +public import Init.Data.Ord.Basic +import all Init.Data.Ord.Basic public section diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 1741d9bfc8..7185dc6c8b 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Floris van Doorn module prelude -public import all Init.Data.Nat.Bitwise.Basic +public import Init.Data.Nat.Bitwise.Basic +import all Init.Data.Nat.Bitwise.Basic public import Init.Data.Nat.MinMax -public import all Init.Data.Nat.Log2 +public import Init.Data.Nat.Log2 +import all Init.Data.Nat.Log2 public import Init.Data.Nat.Power2 public import Init.Data.Nat.Mod diff --git a/src/Init/Data/Option/Array.lean b/src/Init/Data/Option/Array.lean index 181bd55601..17dcc1a06d 100644 --- a/src/Init/Data/Option/Array.lean +++ b/src/Init/Data/Option/Array.lean @@ -8,7 +8,8 @@ module prelude public import Init.Data.Array.Lemmas public import Init.Data.Option.List -public import all Init.Data.Option.Instances +public import Init.Data.Option.Instances +import all Init.Data.Option.Instances public section diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index 9e2e6f0393..37eec8d6ce 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -6,8 +6,10 @@ Authors: Mario Carneiro module prelude -public import all Init.Data.Option.BasicAux -public import all Init.Data.Option.Instances +public import Init.Data.Option.BasicAux +import all Init.Data.Option.BasicAux +public import Init.Data.Option.Instances +import all Init.Data.Option.Instances public import Init.Data.BEq public import Init.Classical public import Init.Ext diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean index 94cf3478f0..5a00b5b7ae 100644 --- a/src/Init/Data/Option/List.lean +++ b/src/Init/Data/Option/List.lean @@ -7,8 +7,10 @@ module prelude public import Init.Data.List.Lemmas -public import all Init.Data.List.Control -public import all Init.Data.Option.Instances +public import Init.Data.List.Control +import all Init.Data.List.Control +public import Init.Data.Option.Instances +import all Init.Data.Option.Instances public section diff --git a/src/Init/Data/Option/Monadic.lean b/src/Init/Data/Option/Monadic.lean index a297f9fc76..8672a1c3a1 100644 --- a/src/Init/Data/Option/Monadic.lean +++ b/src/Init/Data/Option/Monadic.lean @@ -7,7 +7,8 @@ module prelude -public import all Init.Data.Option.Instances +public import Init.Data.Option.Instances +import all Init.Data.Option.Instances public import Init.Data.Option.Attach public import Init.Control.Lawful.Basic diff --git a/src/Init/Data/Ord/Basic.lean b/src/Init/Data/Ord/Basic.lean index d9c32974c6..fa7d4f0641 100644 --- a/src/Init/Data/Ord/Basic.lean +++ b/src/Init/Data/Ord/Basic.lean @@ -9,7 +9,8 @@ prelude public import Init.Data.String.Basic public import Init.Data.Array.Basic public import Init.Data.SInt.Basic -public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public section diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean index 943542a48a..feb58fc78c 100644 --- a/src/Init/Data/Range/Lemmas.lean +++ b/src/Init/Data/Range/Lemmas.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Range.Basic +public import Init.Data.Range.Basic +import all Init.Data.Range.Basic public import Init.Data.List.Range public import Init.Data.List.Monadic public import Init.Data.Nat.Div.Lemmas diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index c193339eaf..508df71fbd 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -8,10 +8,14 @@ module prelude public import Init.Data.Iterators public import Init.Data.Iterators.Lemmas.Consumers.Collect -public import all Init.Data.Range.Polymorphic.Basic -public import all Init.Data.Range.Polymorphic.RangeIterator -public import all Init.Data.Range.Polymorphic.Iterators -public import all Init.Data.Iterators.Consumers.Loop +public import Init.Data.Range.Polymorphic.Basic +import all Init.Data.Range.Polymorphic.Basic +public import Init.Data.Range.Polymorphic.RangeIterator +import all Init.Data.Range.Polymorphic.RangeIterator +public import Init.Data.Range.Polymorphic.Iterators +import all Init.Data.Range.Polymorphic.Iterators +public import Init.Data.Iterators.Consumers.Loop +import all Init.Data.Iterators.Consumers.Loop public section diff --git a/src/Init/Data/SInt/Bitwise.lean b/src/Init/Data/SInt/Bitwise.lean index c75ade05df..32ba7470cb 100644 --- a/src/Init/Data/SInt/Bitwise.lean +++ b/src/Init/Data/SInt/Bitwise.lean @@ -6,11 +6,15 @@ Authors: Markus Himmel module prelude -public import all Init.Data.UInt.Basic +public import Init.Data.UInt.Basic +import all Init.Data.UInt.Basic public import Init.Data.UInt.Bitwise -public import all Init.Data.BitVec.Basic -public import all Init.Data.BitVec.Lemmas -public import all Init.Data.SInt.Basic +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic +public import Init.Data.BitVec.Lemmas +import all Init.Data.BitVec.Lemmas +public import Init.Data.SInt.Basic +import all Init.Data.SInt.Basic public import Init.Data.SInt.Lemmas public section diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean index e572e4b788..9f297c672b 100644 --- a/src/Init/Data/SInt/Lemmas.lean +++ b/src/Init/Data/SInt/Lemmas.lean @@ -6,13 +6,17 @@ Authors: Markus Himmel module prelude -public import all Init.Data.Nat.Bitwise.Basic -public import all Init.Data.SInt.Basic -public import all Init.Data.BitVec.Basic +public import Init.Data.Nat.Bitwise.Basic +import all Init.Data.Nat.Bitwise.Basic +public import Init.Data.SInt.Basic +import all Init.Data.SInt.Basic +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic public import Init.Data.BitVec.Lemmas public import Init.Data.BitVec.Bitblast public import Init.Data.Int.LemmasAux -public import all Init.Data.UInt.Basic +public import Init.Data.UInt.Basic +import all Init.Data.UInt.Basic public import Init.Data.UInt.Lemmas public import Init.System.Platform import Init.Data.Order.Lemmas diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean index 016e1856e7..2776739fa3 100644 --- a/src/Init/Data/Slice/Array/Iterator.lean +++ b/src/Init/Data/Slice/Array/Iterator.lean @@ -13,7 +13,8 @@ import Init.Data.Iterators.Combinators.FilterMap import Init.Data.Iterators.Combinators.ULift public import Init.Data.Iterators.Consumers.Collect public import Init.Data.Iterators.Consumers.Loop -public import all Init.Data.Range.Polymorphic.Basic +public import Init.Data.Range.Polymorphic.Basic +import all Init.Data.Range.Polymorphic.Basic public import Init.Data.Range.Polymorphic.Nat public import Init.Data.Range.Polymorphic.Iterators public import Init.Data.Slice.Operations diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index f01942fcc9..6f57950f83 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -6,11 +6,16 @@ Authors: Paul Reichert module prelude -public import all Init.Data.Array.Subarray -public import all Init.Data.Slice.Array.Basic -public import all Init.Data.Slice.Array.Iterator -public import all Init.Data.Slice.Operations -public import all Init.Data.Range.Polymorphic.Iterators +public import Init.Data.Array.Subarray +import all Init.Data.Array.Subarray +public import Init.Data.Slice.Array.Basic +import all Init.Data.Slice.Array.Basic +public import Init.Data.Slice.Array.Iterator +import all Init.Data.Slice.Array.Iterator +public import Init.Data.Slice.Operations +import all Init.Data.Slice.Operations +public import Init.Data.Range.Polymorphic.Iterators +import all Init.Data.Range.Polymorphic.Iterators public import Init.Data.Range.Polymorphic.Lemmas public import Init.Data.Slice.Lemmas public import Init.Data.Iterators.Lemmas diff --git a/src/Init/Data/Slice/Lemmas.lean b/src/Init/Data/Slice/Lemmas.lean index 00cf83d696..e12971c310 100644 --- a/src/Init/Data/Slice/Lemmas.lean +++ b/src/Init/Data/Slice/Lemmas.lean @@ -6,7 +6,8 @@ Authors: Paul Reichert module prelude -public import all Init.Data.Slice.Operations +public import Init.Data.Slice.Operations +import all Init.Data.Slice.Operations import Init.Data.Iterators.Lemmas.Consumers public section diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index 28638ab329..54b5871ec3 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -6,8 +6,10 @@ Author: Leonardo de Moura module prelude -public import all Init.Data.ByteArray.Basic -public import all Init.Data.String.Basic +public import Init.Data.ByteArray.Basic +import all Init.Data.ByteArray.Basic +public import Init.Data.String.Basic +import all Init.Data.String.Basic public import Init.Data.UInt.Lemmas public section diff --git a/src/Init/Data/Sum/Lemmas.lean b/src/Init/Data/Sum/Lemmas.lean index b46fa443c0..0d4a89b4eb 100644 --- a/src/Init/Data/Sum/Lemmas.lean +++ b/src/Init/Data/Sum/Lemmas.lean @@ -6,7 +6,8 @@ Authors: Mario Carneiro, Yury G. Kudryashov module prelude -public import all Init.Data.Sum.Basic +public import Init.Data.Sum.Basic +import all Init.Data.Sum.Basic public import Init.Ext public section diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean index 4bf2b30e34..a1116fe27d 100644 --- a/src/Init/Data/UInt/Bitwise.lean +++ b/src/Init/Data/UInt/Bitwise.lean @@ -6,8 +6,10 @@ Authors: Markus Himmel, Mac Malone module prelude -public import all Init.Data.BitVec.Basic -public import all Init.Data.UInt.Basic +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic +public import Init.Data.UInt.Basic +import all Init.Data.UInt.Basic public import Init.Data.UInt.Lemmas public import Init.Data.Fin.Bitwise diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index f39bd8d661..cbecdc5288 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -6,12 +6,17 @@ Authors: Leonardo de Moura, François G. Dorais, Mario Carneiro, Mac Malone, Mar module prelude -public import all Init.Data.UInt.Basic -public import all Init.Data.UInt.BasicAux +public import Init.Data.UInt.Basic +import all Init.Data.UInt.Basic +public import Init.Data.UInt.BasicAux +import all Init.Data.UInt.BasicAux public import Init.Data.Fin.Lemmas -public import all Init.Data.Fin.Bitwise -public import all Init.Data.BitVec.BasicAux -public import all Init.Data.BitVec.Basic +public import Init.Data.Fin.Bitwise +import all Init.Data.Fin.Bitwise +public import Init.Data.BitVec.BasicAux +import all Init.Data.BitVec.BasicAux +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic public import Init.Data.BitVec.Lemmas public import Init.Data.Nat.Div.Lemmas public import Init.System.Platform diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean index b3f89acd76..13154481d2 100644 --- a/src/Init/Data/Vector/Attach.lean +++ b/src/Init/Data/Vector/Attach.lean @@ -7,7 +7,8 @@ module prelude public import Init.Data.Vector.Lemmas -public import all Init.Data.Array.Attach +public import Init.Data.Array.Attach +import all Init.Data.Array.Attach public section diff --git a/src/Init/Data/Vector/Count.lean b/src/Init/Data/Vector/Count.lean index b750d07289..7f3834ba14 100644 --- a/src/Init/Data/Vector/Count.lean +++ b/src/Init/Data/Vector/Count.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Count -public import all Init.Data.Vector.Basic +public import Init.Data.Array.Count +import all Init.Data.Array.Count +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas public section diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean index f65459effc..3338b64b27 100644 --- a/src/Init/Data/Vector/Find.lean +++ b/src/Init/Data/Vector/Find.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Basic -public import all Init.Data.Vector.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas public import Init.Data.Vector.Attach public import Init.Data.Vector.Range diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index d5907096ee..7226389ed1 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -6,8 +6,10 @@ Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison module prelude -public import all Init.Data.Array.Basic -public import all Init.Data.Vector.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Array.Attach public import Init.Data.Array.Find diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index 0f77e4f05b..1a3cef8cdf 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas -public import all Init.Data.Array.Lex.Basic +public import Init.Data.Array.Lex.Basic +import all Init.Data.Array.Lex.Basic public import Init.Data.Array.Lex.Lemmas import Init.Data.Range.Polymorphic.Lemmas import Init.Data.Order.Lemmas diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean index 8e355a687b..29731ede3e 100644 --- a/src/Init/Data/Vector/MapIdx.lean +++ b/src/Init/Data/Vector/MapIdx.lean @@ -7,8 +7,10 @@ module prelude public import Init.Data.Array.MapIdx -public import all Init.Data.Array.Basic -public import all Init.Data.Vector.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Attach public import Init.Data.Vector.Lemmas diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index 246984656b..9eca7ac006 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/src/Init/Data/Vector/Monadic.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas public import Init.Data.Vector.Attach public import Init.Data.Array.Monadic diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean index 193e8fe5f1..55b8f2ff05 100644 --- a/src/Init/Data/Vector/OfFn.lean +++ b/src/Init/Data/Vector/OfFn.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas public import Init.Data.Vector.Monadic public import Init.Data.Array.OfFn diff --git a/src/Init/Data/Vector/Perm.lean b/src/Init/Data/Vector/Perm.lean index 4153ebddae..1af501e969 100644 --- a/src/Init/Data/Vector/Perm.lean +++ b/src/Init/Data/Vector/Perm.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Perm -public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas public section diff --git a/src/Init/Data/Vector/Range.lean b/src/Init/Data/Vector/Range.lean index bf8d6f993d..f0a00c5de8 100644 --- a/src/Init/Data/Vector/Range.lean +++ b/src/Init/Data/Vector/Range.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Basic -public import all Init.Data.Vector.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas public import Init.Data.Vector.Zip public import Init.Data.Vector.MapIdx diff --git a/src/Init/Data/Vector/Zip.lean b/src/Init/Data/Vector/Zip.lean index 13b48eb9d9..58d1c139be 100644 --- a/src/Init/Data/Vector/Zip.lean +++ b/src/Init/Data/Vector/Zip.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -public import all Init.Data.Array.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Data.Array.Zip -public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Basic +import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas public section diff --git a/src/Init/Grind/Module/Basic.lean b/src/Init/Grind/Module/Basic.lean index 1ea52d0c8f..f6480221f6 100644 --- a/src/Init/Grind/Module/Basic.lean +++ b/src/Init/Grind/Module/Basic.lean @@ -7,7 +7,8 @@ module prelude public import Init.Data.Int.Order -public import all Init.Grind.ToInt +public import Init.Grind.ToInt +import all Init.Grind.ToInt public section diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean index df4a6fb34a..6710887268 100644 --- a/src/Init/Grind/Module/Envelope.lean +++ b/src/Init/Grind/Module/Envelope.lean @@ -7,7 +7,8 @@ module prelude public import Init.Grind.Ordered.Module -public import all Init.Data.AC +public import Init.Data.AC +import all Init.Data.AC public section diff --git a/src/Init/Grind/Ordered/Linarith.lean b/src/Init/Grind/Ordered/Linarith.lean index e9cea89c81..ec4b383251 100644 --- a/src/Init/Grind/Ordered/Linarith.lean +++ b/src/Init/Grind/Ordered/Linarith.lean @@ -8,8 +8,10 @@ prelude public import Init.Grind.Ordered.Module public import Init.Grind.Ordered.Ring public import Init.Grind.Ring.Field -public import all Init.Data.Ord.Basic -public import all Init.Data.AC +public import Init.Data.Ord.Basic +import all Init.Data.Ord.Basic +public import Init.Data.AC +import all Init.Data.AC public import Init.Data.RArray @[expose] public section diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean index e9a56ea70d..082cb405d6 100644 --- a/src/Init/Grind/Ring/Envelope.lean +++ b/src/Init/Grind/Ring/Envelope.lean @@ -8,7 +8,8 @@ module prelude public import Init.Grind.Ring.Basic public import Init.Grind.Ordered.Ring -public import all Init.Data.AC +public import Init.Data.AC +import all Init.Data.AC @[expose] public section diff --git a/src/Init/Grind/Ring/Poly.lean b/src/Init/Grind/Ring/Poly.lean index 488c9f7a94..8abcc5d585 100644 --- a/src/Init/Grind/Ring/Poly.lean +++ b/src/Init/Grind/Ring/Poly.lean @@ -9,7 +9,8 @@ prelude public import Init.Data.Nat.Lemmas public import Init.Data.Int.LemmasAux public import Init.Data.Hashable -public import all Init.Data.Ord.Basic +public import Init.Data.Ord.Basic +import all Init.Data.Ord.Basic public import Init.Data.RArray public import Init.Grind.Ring.Basic public import Init.Grind.Ring.Field diff --git a/src/Init/Grind/ToIntLemmas.lean b/src/Init/Grind/ToIntLemmas.lean index e1fa458b46..6f281655f5 100644 --- a/src/Init/Grind/ToIntLemmas.lean +++ b/src/Init/Grind/ToIntLemmas.lean @@ -6,7 +6,8 @@ Authors: Leonardo de Moura module prelude -public import all Init.Grind.ToInt +public import Init.Grind.ToInt +import all Init.Grind.ToInt public section diff --git a/src/Init/GrindInstances/Ring/BitVec.lean b/src/Init/GrindInstances/Ring/BitVec.lean index 599f166f77..5205394263 100644 --- a/src/Init/GrindInstances/Ring/BitVec.lean +++ b/src/Init/GrindInstances/Ring/BitVec.lean @@ -9,8 +9,10 @@ prelude public import Init.Grind.Ring.Basic public import Init.Grind.Ordered.Order public import Init.GrindInstances.ToInt -public import all Init.Data.BitVec.Basic -public import all Init.Grind.ToInt +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic +public import Init.Grind.ToInt +import all Init.Grind.ToInt public section diff --git a/src/Init/GrindInstances/Ring/Fin.lean b/src/Init/GrindInstances/Ring/Fin.lean index 578a2f51aa..68c256c94d 100644 --- a/src/Init/GrindInstances/Ring/Fin.lean +++ b/src/Init/GrindInstances/Ring/Fin.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -public import all Init.Data.Zero +public import Init.Data.Zero +import all Init.Data.Zero public import Init.Grind.Ring.Basic -public import all Init.GrindInstances.ToInt +public import Init.GrindInstances.ToInt +import all Init.GrindInstances.ToInt public import Init.Data.Fin.Lemmas public section diff --git a/src/Init/GrindInstances/Ring/SInt.lean b/src/Init/GrindInstances/Ring/SInt.lean index 80ce86a471..308d26be3e 100644 --- a/src/Init/GrindInstances/Ring/SInt.lean +++ b/src/Init/GrindInstances/Ring/SInt.lean @@ -7,10 +7,13 @@ module prelude public import Init.Grind.Ring.Basic -public import all Init.Grind.ToInt +public import Init.Grind.ToInt +import all Init.Grind.ToInt public import Init.GrindInstances.ToInt -public import all Init.Data.BitVec.Basic -public import all Init.Data.SInt.Basic +public import Init.Data.BitVec.Basic +import all Init.Data.BitVec.Basic +public import Init.Data.SInt.Basic +import all Init.Data.SInt.Basic public import Init.Data.SInt.Lemmas public section diff --git a/src/Init/GrindInstances/Ring/UInt.lean b/src/Init/GrindInstances/Ring/UInt.lean index 5e3139c8d1..f55327131f 100644 --- a/src/Init/GrindInstances/Ring/UInt.lean +++ b/src/Init/GrindInstances/Ring/UInt.lean @@ -7,8 +7,10 @@ module prelude public import Init.Grind.Ring.Basic -public import all Init.GrindInstances.ToInt -public import all Init.Data.UInt.Basic +public import Init.GrindInstances.ToInt +import all Init.GrindInstances.ToInt +public import Init.Data.UInt.Basic +import all Init.Data.UInt.Basic public import Init.Data.UInt.Lemmas public section diff --git a/src/Init/GrindInstances/ToInt.lean b/src/Init/GrindInstances/ToInt.lean index 83c5a46e57..4f531c5b95 100644 --- a/src/Init/GrindInstances/ToInt.lean +++ b/src/Init/GrindInstances/ToInt.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Grind.ToInt +public import Init.Grind.ToInt +import all Init.Grind.ToInt public import Init.Grind.Module.Basic public import Init.Grind.Ring.ToInt public import Init.Data.Int.DivMod.Basic diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index 4ef3dbbfcc..af7e3472f5 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -9,7 +9,8 @@ prelude public import Init.ByCases public import Init.RCases -public import all Init.Control.Except -- for `MonoBind` instance +public import Init.Control.Except -- for `MonoBind` instance +import all Init.Control.Except -- for `MonoBind` instance public section diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean index d82c12a482..a0d5183068 100644 --- a/src/Init/Internal/Order/Lemmas.lean +++ b/src/Init/Internal/Order/Lemmas.lean @@ -8,9 +8,12 @@ module prelude -public import all Init.Data.List.Control -public import all Init.Data.Option.Basic -public import all Init.Data.Array.Basic +public import Init.Data.List.Control +import all Init.Data.List.Control +public import Init.Data.Option.Basic +import all Init.Data.Option.Basic +public import Init.Data.Array.Basic +import all Init.Data.Array.Basic public import Init.Internal.Order.Basic public section diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 8ca34738a4..88acee7b66 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -8,7 +8,8 @@ Additional goodies for writing macros module prelude -public import all Init.Prelude -- for unfolding `Name.beq` +public import Init.Prelude -- for unfolding `Name.beq` +import all Init.Prelude -- for unfolding `Name.beq` public import Init.MetaTypes public import Init.Syntax public import Init.Data.Array.GetLit diff --git a/src/Init/Omega/Coeffs.lean b/src/Init/Omega/Coeffs.lean index 848b6ddf2a..609a89e2c9 100644 --- a/src/Init/Omega/Coeffs.lean +++ b/src/Init/Omega/Coeffs.lean @@ -6,7 +6,8 @@ Authors: Kim Morrison module prelude -public import all Init.Omega.IntList +public import Init.Omega.IntList +import all Init.Omega.IntList public section diff --git a/src/Init/SizeOfLemmas.lean b/src/Init/SizeOfLemmas.lean index 22fe959295..fae685f20e 100644 --- a/src/Init/SizeOfLemmas.lean +++ b/src/Init/SizeOfLemmas.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -public import all Init.Data.Char.Basic +public import Init.Data.Char.Basic +import all Init.Data.Char.Basic public import Init.Meta -public import all Init.SizeOf +public import Init.SizeOf +import all Init.SizeOf public import Init.Data.Nat.Linear public section diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index e4fc59cdc0..bfb1750ece 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -89,24 +89,32 @@ def parseHeader (inputCtx : InputContext) : IO (TSyntax ``Module.header × Modul for (pos, stk, err) in s.allErrors do messages := messages.add <| mkErrorMessage inputCtx pos stk err if let `(Module.header| $[module%$moduleTk?]? $[prelude]? $importsStx*) := stx then - if moduleTk?.isNone then - let mkError ref msg : Message := - let pos := ref.getPos?.getD 0 - { - fileName := inputCtx.fileName - pos := inputCtx.fileMap.toPosition pos - endPos := inputCtx.fileMap.toPosition <| ref.getTailPos?.getD pos - keepFullRange := true - data := msg - } - for stx in importsStx do - if let `(Module.import| $[public%$pubTk?]? $[meta%$metaTk?]? import $[all%$allTk?]? $_) := stx then + let mkError ref msg : Message := + let pos := ref.getPos?.getD 0 + { + fileName := inputCtx.fileName + pos := inputCtx.fileMap.toPosition pos + endPos := inputCtx.fileMap.toPosition <| ref.getTailPos?.getD pos + keepFullRange := true + data := msg + } + for stx in importsStx do + if let `(Module.import| $[public%$pubTk?]? $[meta%$metaTk?]? import $[all%$allTk?]? $mod) := stx then + let mod := mod.getId + if moduleTk?.isNone then if let some tk := pubTk? then - messages := messages.add <| mkError tk "cannot use 'public import' without 'module'" + messages := messages.add <| mkError tk "cannot use `public import` without `module`" if let some tk := metaTk? then - messages := messages.add <| mkError tk "cannot use 'meta import' without 'module'" + messages := messages.add <| mkError tk "cannot use `meta import` without `module`" if let some tk := allTk? then - messages := messages.add <| mkError tk "cannot use 'import all' without 'module'" + messages := messages.add <| mkError tk "cannot use `import all` without `module`" + else + if let some tk := allTk? then + if pubTk?.isSome then + messages := messages.add <| mkError tk s!"cannot use `all` with `public import`; \ + consider using separate `public import {mod}` and `import all {mod}` directives \ + in order to import public data into the public scope and private data into the \ + private scope." pure (⟨stx⟩, {pos := s.pos, recovering := s.hasError}, messages) private def mkEOI (pos : String.Pos) : Syntax := diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 5ed7a58f06..5e2aaa79a1 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -6,7 +6,8 @@ Authors: Markus Himmel module prelude -public import all Std.Data.DHashMap.Raw +public import Std.Data.DHashMap.Raw +import all Std.Data.DHashMap.Raw public section diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index ae2ffdf859..3144ee5964 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean @@ -6,7 +6,8 @@ Authors: Markus Himmel module prelude -public import all Std.Data.DHashMap.Internal.AssocList.Basic +public import Std.Data.DHashMap.Internal.AssocList.Basic +import all Std.Data.DHashMap.Internal.AssocList.Basic public import Std.Data.Internal.List.Associative public section diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index d8c9f6ba68..3a6e1bd59d 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -8,7 +8,8 @@ module prelude public import Init.Data.Array.TakeDrop public import Std.Data.DHashMap.Basic -public import all Std.Data.DHashMap.Internal.Defs +public import Std.Data.DHashMap.Internal.Defs +import all Std.Data.DHashMap.Internal.Defs public import Std.Data.DHashMap.Internal.HashesTo public import Std.Data.DHashMap.Internal.AssocList.Lemmas diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean index effc801196..10ed682a1a 100644 --- a/src/Std/Data/DHashMap/Internal/Raw.lean +++ b/src/Std/Data/DHashMap/Internal/Raw.lean @@ -6,7 +6,8 @@ Authors: Markus Himmel module prelude -public import all Std.Data.DHashMap.Basic +public import Std.Data.DHashMap.Basic +import all Std.Data.DHashMap.Basic public section diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 40715fc684..4d85c44746 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -9,7 +9,8 @@ prelude public import Std.Data.DHashMap.Internal.Raw public import Std.Data.DHashMap.Internal.RawLemmas import all Std.Data.DHashMap.Basic -public import all Std.Data.DHashMap.AdditionalOperations +public import Std.Data.DHashMap.AdditionalOperations +import all Std.Data.DHashMap.AdditionalOperations public section diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index f013ee6dd6..4fa32ca32e 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -8,7 +8,8 @@ module prelude public import Std.Data.DHashMap.Internal.Raw public import Std.Data.DHashMap.Internal.RawLemmas -public import all Std.Data.DHashMap.Raw +public import Std.Data.DHashMap.Raw +import all Std.Data.DHashMap.Raw public section diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 49d28e41b3..12e5f52332 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -13,7 +13,8 @@ public import Init.Data.List.Perm public import Init.Data.List.Find public import Init.Data.List.MinMax public import Init.Data.List.Monadic -public import all Std.Data.Internal.List.Defs +public import Std.Data.Internal.List.Defs +import all Std.Data.Internal.List.Defs public import Init.Data.Order.Ord import Init.Data.Subtype.Order import Init.Data.Order.Lemmas diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean index 3f839cdf5e..809bff7f69 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean @@ -6,7 +6,8 @@ Authors: Paul Reichert module prelude -public import all Std.Data.Iterators.Producers.Slice +public import Std.Data.Iterators.Producers.Slice +import all Std.Data.Iterators.Producers.Slice public import Init.Data.Slice.Lemmas @[expose] public section diff --git a/src/Std/Time/Date/ValidDate.lean b/src/Std/Time/Date/ValidDate.lean index e4338e0415..e6dc6cba2e 100644 --- a/src/Std/Time/Date/ValidDate.lean +++ b/src/Std/Time/Date/ValidDate.lean @@ -8,7 +8,8 @@ module prelude public import Std.Internal.Rat public import Std.Time.Date.Unit.Day -public import all Std.Time.Date.Unit.Month +public import Std.Time.Date.Unit.Month +import all Std.Time.Date.Unit.Month public section diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean index fa247f2bc2..f0a3ae0faa 100644 --- a/src/Std/Time/Format.lean +++ b/src/Std/Time/Format.lean @@ -7,7 +7,8 @@ module prelude public import Std.Time.Notation.Spec -public import all Std.Time.Format.Basic +public import Std.Time.Format.Basic +import all Std.Time.Format.Basic public import Std.Time.Internal.Bounded public section diff --git a/tests/lean/moduleKeywords.lean.expected.out b/tests/lean/moduleKeywords.lean.expected.out index 12713c9fb0..e94adb5ff8 100644 --- a/tests/lean/moduleKeywords.lean.expected.out +++ b/tests/lean/moduleKeywords.lean.expected.out @@ -1,3 +1,3 @@ -moduleKeywords.lean:1:0-1:6: error: cannot use 'public import' without 'module' -moduleKeywords.lean:1:7-1:11: error: cannot use 'meta import' without 'module' -moduleKeywords.lean:2:7-2:10: error: cannot use 'import all' without 'module' +moduleKeywords.lean:1:0-1:6: error: cannot use `public import` without `module` +moduleKeywords.lean:1:7-1:11: error: cannot use `meta import` without `module` +moduleKeywords.lean:2:7-2:10: error: cannot use `import all` without `module` diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index c763a59663..ce2d845d65 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/tests/pkg/module/Module/ImportedAll.lean @@ -1,6 +1,7 @@ module -public import all Module.Basic +public import Module.Basic +import all Module.Basic import Lean.CoreM /-! `import all` should import private information, privately. -/ diff --git a/tests/pkg/module/Module/ImportedAllPrivateImported.lean b/tests/pkg/module/Module/ImportedAllPrivateImported.lean index e71e2fb8b2..0d0c81d15d 100644 --- a/tests/pkg/module/Module/ImportedAllPrivateImported.lean +++ b/tests/pkg/module/Module/ImportedAllPrivateImported.lean @@ -1,7 +1,8 @@ module prelude -public import all Module.PrivateImported +public import Module.PrivateImported +import all Module.PrivateImported /-! `import all` should activate nested `private import`s. -/