From 09a5b349314c2b6e42c6293d215de994397d0377 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 28 Jun 2025 18:30:53 +0200 Subject: [PATCH] feat: make `private` the default in `module` (#9044) This PR adjusts the experimental module system to make `private` the default visibility modifier in `module`s, introducing `public` as a new modifier instead. `public section` can be used to revert the default for an entire section, though this is more intended to ease gradual adoption of the new semantics such as in `Init` (and soon `Std`) where they should be replaced by a future decl-by-decl re-review of visibilities. --- src/Init/BinderNameHint.lean | 6 +- src/Init/BinderPredicates.lean | 4 +- src/Init/ByCases.lean | 4 +- src/Init/Classical.lean | 4 +- src/Init/Coe.lean | 6 +- src/Init/Control.lean | 22 ++--- src/Init/Control/Basic.lean | 6 +- src/Init/Control/EState.lean | 8 +- src/Init/Control/Except.lean | 8 +- src/Init/Control/ExceptCps.lean | 4 +- src/Init/Control/Id.lean | 4 +- src/Init/Control/Lawful.lean | 10 ++- src/Init/Control/Lawful/Basic.lean | 8 +- src/Init/Control/Lawful/Instances.lean | 12 +-- src/Init/Control/Lawful/Lemmas.lean | 8 +- src/Init/Control/Lawful/MonadLift.lean | 8 +- src/Init/Control/Lawful/MonadLift/Basic.lean | 4 +- .../Control/Lawful/MonadLift/Instances.lean | 18 ++-- src/Init/Control/Lawful/MonadLift/Lemmas.lean | 6 +- src/Init/Control/Option.lean | 8 +- src/Init/Control/Reader.lean | 8 +- src/Init/Control/State.lean | 8 +- src/Init/Control/StateCps.lean | 4 +- src/Init/Control/StateRef.lean | 4 +- src/Init/Conv.lean | 6 +- src/Init/Core.lean | 6 +- src/Init/Data.lean | 88 ++++++++++--------- src/Init/Data/AC.lean | 6 +- src/Init/Data/Array.lean | 50 ++++++----- src/Init/Data/Array/Attach.lean | 10 ++- src/Init/Data/Array/Basic.lean | 20 +++-- src/Init/Data/Array/BasicAux.lean | 8 +- src/Init/Data/Array/BinSearch.lean | 8 +- src/Init/Data/Array/Bootstrap.lean | 6 +- src/Init/Data/Array/Count.lean | 8 +- src/Init/Data/Array/DecidableEq.lean | 10 ++- src/Init/Data/Array/Erase.lean | 10 ++- src/Init/Data/Array/Extract.lean | 6 +- src/Init/Data/Array/FinRange.lean | 6 +- src/Init/Data/Array/Find.lean | 12 +-- src/Init/Data/Array/GetLit.lean | 4 +- src/Init/Data/Array/InsertIdx.lean | 6 +- src/Init/Data/Array/InsertionSort.lean | 4 +- src/Init/Data/Array/Lemmas.lean | 32 +++---- src/Init/Data/Array/Lex.lean | 6 +- src/Init/Data/Array/Lex/Basic.lean | 8 +- src/Init/Data/Array/Lex/Lemmas.lean | 8 +- src/Init/Data/Array/MapIdx.lean | 12 +-- src/Init/Data/Array/Mem.lean | 8 +- src/Init/Data/Array/Monadic.lean | 12 +-- src/Init/Data/Array/OfFn.lean | 12 +-- src/Init/Data/Array/Perm.lean | 8 +- src/Init/Data/Array/QSort.lean | 4 +- src/Init/Data/Array/QSort/Basic.lean | 6 +- src/Init/Data/Array/Range.lean | 14 +-- src/Init/Data/Array/Set.lean | 4 +- src/Init/Data/Array/Subarray.lean | 6 +- src/Init/Data/Array/Subarray/Split.lean | 8 +- src/Init/Data/Array/TakeDrop.lean | 8 +- src/Init/Data/Array/Zip.lean | 8 +- src/Init/Data/BEq.lean | 4 +- src/Init/Data/Basic.lean | 22 ++--- src/Init/Data/BitVec.lean | 16 ++-- src/Init/Data/BitVec/Basic.lean | 12 +-- src/Init/Data/BitVec/BasicAux.lean | 4 +- src/Init/Data/BitVec/Bitblast.lean | 18 ++-- src/Init/Data/BitVec/Bootstrap.lean | 4 +- src/Init/Data/BitVec/Decidable.lean | 4 +- src/Init/Data/BitVec/Folds.lean | 10 ++- src/Init/Data/BitVec/Lemmas.lean | 28 +++--- src/Init/Data/Bool.lean | 4 +- src/Init/Data/ByteArray.lean | 4 +- src/Init/Data/ByteArray/Basic.lean | 10 ++- src/Init/Data/Cast.lean | 4 +- src/Init/Data/Char.lean | 6 +- src/Init/Data/Char/Basic.lean | 4 +- src/Init/Data/Char/Lemmas.lean | 6 +- src/Init/Data/Fin.lean | 12 +-- src/Init/Data/Fin/Basic.lean | 4 +- src/Init/Data/Fin/Bitwise.lean | 6 +- src/Init/Data/Fin/Fold.lean | 8 +- src/Init/Data/Fin/Iterate.lean | 6 +- src/Init/Data/Fin/Lemmas.lean | 14 +-- src/Init/Data/Fin/Log2.lean | 4 +- src/Init/Data/Float.lean | 8 +- src/Init/Data/Float32.lean | 10 ++- src/Init/Data/FloatArray.lean | 4 +- src/Init/Data/FloatArray/Basic.lean | 8 +- src/Init/Data/Format.lean | 10 ++- src/Init/Data/Format/Basic.lean | 8 +- src/Init/Data/Format/Instances.lean | 8 +- src/Init/Data/Format/Macro.lean | 6 +- src/Init/Data/Format/Syntax.lean | 8 +- src/Init/Data/Function.lean | 4 +- src/Init/Data/Hashable.lean | 8 +- src/Init/Data/Int.lean | 26 +++--- src/Init/Data/Int/Basic.lean | 6 +- src/Init/Data/Int/Bitwise.lean | 6 +- src/Init/Data/Int/Bitwise/Basic.lean | 6 +- src/Init/Data/Int/Bitwise/Lemmas.lean | 8 +- src/Init/Data/Int/Compare.lean | 6 +- src/Init/Data/Int/Cooper.lean | 6 +- src/Init/Data/Int/DivMod.lean | 8 +- src/Init/Data/Int/DivMod/Basic.lean | 4 +- src/Init/Data/Int/DivMod/Bootstrap.lean | 10 ++- src/Init/Data/Int/DivMod/Lemmas.lean | 16 ++-- src/Init/Data/Int/Gcd.lean | 12 +-- src/Init/Data/Int/Lemmas.lean | 8 +- src/Init/Data/Int/LemmasAux.lean | 10 ++- src/Init/Data/Int/Linear.lean | 20 +++-- src/Init/Data/Int/OfNat.lean | 10 ++- src/Init/Data/Int/Order.lean | 6 +- src/Init/Data/Int/Pow.lean | 6 +- src/Init/Data/Iterators.lean | 16 ++-- src/Init/Data/Iterators/Basic.lean | 12 +-- src/Init/Data/Iterators/Combinators.lean | 8 +- .../Data/Iterators/Combinators/Attach.lean | 6 +- .../Data/Iterators/Combinators/FilterMap.lean | 4 +- .../Data/Iterators/Combinators/Monadic.lean | 6 +- .../Iterators/Combinators/Monadic/Attach.lean | 10 ++- .../Combinators/Monadic/FilterMap.lean | 12 +-- .../Iterators/Combinators/Monadic/ULift.lean | 8 +- .../Data/Iterators/Combinators/ULift.lean | 4 +- src/Init/Data/Iterators/Consumers.lean | 12 +-- src/Init/Data/Iterators/Consumers/Access.lean | 10 ++- .../Data/Iterators/Consumers/Collect.lean | 8 +- src/Init/Data/Iterators/Consumers/Loop.lean | 8 +- .../Data/Iterators/Consumers/Monadic.lean | 10 ++- .../Iterators/Consumers/Monadic/Access.lean | 4 +- .../Iterators/Consumers/Monadic/Collect.lean | 6 +- .../Iterators/Consumers/Monadic/Loop.lean | 8 +- .../Iterators/Consumers/Monadic/Partial.lean | 4 +- .../Data/Iterators/Consumers/Partial.lean | 4 +- src/Init/Data/Iterators/Internal.lean | 6 +- .../Internal/LawfulMonadLiftFunction.lean | 10 ++- .../Data/Iterators/Internal/Termination.lean | 4 +- src/Init/Data/Iterators/Lemmas.lean | 6 +- src/Init/Data/Iterators/Lemmas/Basic.lean | 4 +- .../Data/Iterators/Lemmas/Combinators.lean | 10 ++- .../Iterators/Lemmas/Combinators/Attach.lean | 10 ++- .../Lemmas/Combinators/FilterMap.lean | 8 +- .../Iterators/Lemmas/Combinators/Monadic.lean | 8 +- .../Lemmas/Combinators/Monadic/Attach.lean | 6 +- .../Lemmas/Combinators/Monadic/FilterMap.lean | 10 ++- .../Lemmas/Combinators/Monadic/ULift.lean | 6 +- .../Iterators/Lemmas/Combinators/ULift.lean | 8 +- src/Init/Data/Iterators/Lemmas/Consumers.lean | 8 +- .../Iterators/Lemmas/Consumers/Collect.lean | 10 ++- .../Data/Iterators/Lemmas/Consumers/Loop.lean | 10 ++- .../Iterators/Lemmas/Consumers/Monadic.lean | 6 +- .../Lemmas/Consumers/Monadic/Collect.lean | 8 +- .../Lemmas/Consumers/Monadic/Loop.lean | 6 +- .../Data/Iterators/Lemmas/Monadic/Basic.lean | 4 +- .../Data/Iterators/PostconditionMonad.lean | 8 +- src/Init/Data/Iterators/ToIterator.lean | 4 +- src/Init/Data/List.lean | 52 +++++------ src/Init/Data/List/Attach.lean | 10 ++- src/Init/Data/List/Basic.lean | 10 ++- src/Init/Data/List/BasicAux.lean | 4 +- src/Init/Data/List/Control.lean | 8 +- src/Init/Data/List/Count.lean | 4 +- src/Init/Data/List/Erase.lean | 6 +- src/Init/Data/List/FinRange.lean | 6 +- src/Init/Data/List/Find.lean | 14 +-- src/Init/Data/List/Impl.lean | 4 +- src/Init/Data/List/Lemmas.lean | 14 +-- src/Init/Data/List/Lex.lean | 6 +- src/Init/Data/List/MapIdx.lean | 12 +-- src/Init/Data/List/MinMax.lean | 6 +- src/Init/Data/List/Monadic.lean | 12 +-- src/Init/Data/List/Nat.lean | 26 +++--- src/Init/Data/List/Nat/BEq.lean | 6 +- src/Init/Data/List/Nat/Basic.lean | 10 ++- src/Init/Data/List/Nat/Count.lean | 6 +- src/Init/Data/List/Nat/Erase.lean | 6 +- src/Init/Data/List/Nat/Find.lean | 6 +- src/Init/Data/List/Nat/InsertIdx.lean | 4 +- src/Init/Data/List/Nat/Modify.lean | 6 +- src/Init/Data/List/Nat/Pairwise.lean | 8 +- src/Init/Data/List/Nat/Perm.lean | 6 +- src/Init/Data/List/Nat/Range.lean | 12 +-- src/Init/Data/List/Nat/Sublist.lean | 10 ++- src/Init/Data/List/Nat/TakeDrop.lean | 10 ++- src/Init/Data/List/Notation.lean | 4 +- src/Init/Data/List/OfFn.lean | 6 +- src/Init/Data/List/Pairwise.lean | 6 +- src/Init/Data/List/Perm.lean | 10 ++- src/Init/Data/List/Range.lean | 6 +- src/Init/Data/List/Sort.lean | 8 +- src/Init/Data/List/Sort/Basic.lean | 6 +- src/Init/Data/List/Sort/Impl.lean | 6 +- src/Init/Data/List/Sort/Lemmas.lean | 10 ++- src/Init/Data/List/Sublist.lean | 4 +- src/Init/Data/List/TakeDrop.lean | 6 +- src/Init/Data/List/ToArray.lean | 18 ++-- src/Init/Data/List/ToArrayImpl.lean | 4 +- src/Init/Data/List/Zip.lean | 6 +- src/Init/Data/Nat.lean | 36 ++++---- src/Init/Data/Nat/Basic.lean | 8 +- src/Init/Data/Nat/Bitwise.lean | 6 +- src/Init/Data/Nat/Bitwise/Basic.lean | 8 +- src/Init/Data/Nat/Bitwise/Lemmas.lean | 14 +-- src/Init/Data/Nat/Compare.lean | 4 +- src/Init/Data/Nat/Control.lean | 8 +- src/Init/Data/Nat/Div.lean | 6 +- src/Init/Data/Nat/Div/Basic.lean | 10 ++- src/Init/Data/Nat/Div/Lemmas.lean | 8 +- src/Init/Data/Nat/Dvd.lean | 6 +- src/Init/Data/Nat/Fold.lean | 6 +- src/Init/Data/Nat/Gcd.lean | 8 +- src/Init/Data/Nat/Lcm.lean | 6 +- src/Init/Data/Nat/Lemmas.lean | 12 +-- src/Init/Data/Nat/Linear.lean | 8 +- src/Init/Data/Nat/Log2.lean | 4 +- src/Init/Data/Nat/MinMax.lean | 4 +- src/Init/Data/Nat/Mod.lean | 4 +- src/Init/Data/Nat/Power2.lean | 4 +- src/Init/Data/Nat/SOM.lean | 6 +- src/Init/Data/Nat/Simproc.lean | 8 +- src/Init/Data/NeZero.lean | 4 +- src/Init/Data/OfScientific.lean | 10 ++- src/Init/Data/Option.lean | 20 +++-- src/Init/Data/Option/Array.lean | 8 +- src/Init/Data/Option/Attach.lean | 14 +-- src/Init/Data/Option/Basic.lean | 4 +- src/Init/Data/Option/BasicAux.lean | 6 +- src/Init/Data/Option/Coe.lean | 4 +- src/Init/Data/Option/Instances.lean | 4 +- src/Init/Data/Option/Lemmas.lean | 12 +-- src/Init/Data/Option/List.lean | 8 +- src/Init/Data/Option/Monadic.lean | 8 +- src/Init/Data/Ord.lean | 10 ++- src/Init/Data/PLift.lean | 4 +- src/Init/Data/Prod.lean | 6 +- src/Init/Data/Queue.lean | 4 +- src/Init/Data/RArray.lean | 4 +- src/Init/Data/Random.lean | 4 +- src/Init/Data/Range.lean | 6 +- src/Init/Data/Range/Basic.lean | 6 +- src/Init/Data/Range/Lemmas.lean | 10 ++- src/Init/Data/Range/Polymorphic.lean | 12 +-- src/Init/Data/Range/Polymorphic/Basic.lean | 4 +- .../Data/Range/Polymorphic/Iterators.lean | 10 ++- src/Init/Data/Range/Polymorphic/Lemmas.lean | 14 +-- src/Init/Data/Range/Polymorphic/Nat.lean | 6 +- .../Data/Range/Polymorphic/NatLemmas.lean | 6 +- src/Init/Data/Range/Polymorphic/PRange.lean | 6 +- .../Data/Range/Polymorphic/RangeIterator.lean | 14 +-- .../Range/Polymorphic/UpwardEnumerable.lean | 10 ++- src/Init/Data/Repr.lean | 4 +- src/Init/Data/SInt.lean | 12 +-- src/Init/Data/SInt/Basic.lean | 4 +- src/Init/Data/SInt/Bitwise.lean | 14 +-- src/Init/Data/SInt/Float.lean | 6 +- src/Init/Data/SInt/Float32.lean | 6 +- src/Init/Data/SInt/Lemmas.lean | 20 +++-- src/Init/Data/Slice.lean | 10 ++- src/Init/Data/Slice/Array.lean | 8 +- src/Init/Data/Slice/Array/Basic.lean | 10 ++- src/Init/Data/Slice/Array/Iterator.lean | 18 ++-- src/Init/Data/Slice/Array/Lemmas.lean | 18 ++-- src/Init/Data/Slice/Basic.lean | 4 +- src/Init/Data/Slice/Lemmas.lean | 4 +- src/Init/Data/Slice/Notation.lean | 4 +- src/Init/Data/Slice/Operations.lean | 8 +- src/Init/Data/Stream.lean | 9 +- src/Init/Data/String.lean | 8 +- src/Init/Data/String/Basic.lean | 6 +- src/Init/Data/String/Extra.lean | 8 +- src/Init/Data/String/Lemmas.lean | 6 +- src/Init/Data/Subtype.lean | 6 +- src/Init/Data/Sum.lean | 6 +- src/Init/Data/Sum/Basic.lean | 4 +- src/Init/Data/Sum/Lemmas.lean | 6 +- src/Init/Data/ToString.lean | 6 +- src/Init/Data/ToString/Basic.lean | 6 +- src/Init/Data/ToString/Macro.lean | 4 +- src/Init/Data/UInt.lean | 12 +-- src/Init/Data/UInt/Basic.lean | 6 +- src/Init/Data/UInt/BasicAux.lean | 6 +- src/Init/Data/UInt/Bitwise.lean | 10 ++- src/Init/Data/UInt/Lemmas.lean | 20 +++-- src/Init/Data/UInt/Log2.lean | 4 +- src/Init/Data/ULift.lean | 4 +- src/Init/Data/Vector.lean | 34 +++---- src/Init/Data/Vector/Attach.lean | 6 +- src/Init/Data/Vector/Basic.lean | 18 ++-- src/Init/Data/Vector/Count.lean | 8 +- src/Init/Data/Vector/DecidableEq.lean | 6 +- src/Init/Data/Vector/Erase.lean | 6 +- src/Init/Data/Vector/Extract.lean | 6 +- src/Init/Data/Vector/FinRange.lean | 6 +- src/Init/Data/Vector/Find.lean | 14 +-- src/Init/Data/Vector/InsertIdx.lean | 6 +- src/Init/Data/Vector/Lemmas.lean | 10 ++- src/Init/Data/Vector/Lex.lean | 10 ++- src/Init/Data/Vector/MapIdx.lean | 12 +-- src/Init/Data/Vector/Monadic.lean | 12 +-- src/Init/Data/Vector/OfFn.lean | 10 ++- src/Init/Data/Vector/Perm.lean | 10 ++- src/Init/Data/Vector/Range.lean | 14 +-- src/Init/Data/Vector/Zip.lean | 10 ++- src/Init/Data/Zero.lean | 4 +- src/Init/Dynamic.lean | 4 +- src/Init/Ext.lean | 8 +- src/Init/GetElem.lean | 4 +- src/Init/Grind.lean | 32 +++---- src/Init/Grind/Cases.lean | 6 +- src/Init/Grind/Ext.lean | 6 +- src/Init/Grind/Lemmas.lean | 12 +-- src/Init/Grind/Module.lean | 6 +- src/Init/Grind/Module/Basic.lean | 6 +- src/Init/Grind/Module/Envelope.lean | 6 +- src/Init/Grind/Norm.lean | 16 ++-- src/Init/Grind/Offset.lean | 6 +- src/Init/Grind/Ordered.lean | 14 +-- src/Init/Grind/Ordered/Field.lean | 6 +- src/Init/Grind/Ordered/Int.lean | 8 +- src/Init/Grind/Ordered/Linarith.lean | 14 +-- src/Init/Grind/Ordered/Module.lean | 8 +- src/Init/Grind/Ordered/Order.lean | 4 +- src/Init/Grind/Ordered/Ring.lean | 6 +- src/Init/Grind/PP.lean | 4 +- src/Init/Grind/Propagator.lean | 4 +- src/Init/Grind/Ring.lean | 14 +-- src/Init/Grind/Ring/Basic.lean | 12 +-- src/Init/Grind/Ring/Envelope.lean | 8 +- src/Init/Grind/Ring/Field.lean | 4 +- src/Init/Grind/Ring/OfSemiring.lean | 10 ++- src/Init/Grind/Ring/Poly.lean | 16 ++-- src/Init/Grind/Ring/ToInt.lean | 6 +- src/Init/Grind/Tactics.lean | 4 +- src/Init/Grind/ToInt.lean | 4 +- src/Init/Grind/ToIntLemmas.lean | 4 +- src/Init/Grind/Util.lean | 6 +- src/Init/GrindInstances.lean | 8 +- src/Init/GrindInstances/Nat.lean | 6 +- src/Init/GrindInstances/Ring.lean | 14 +-- src/Init/GrindInstances/Ring/BitVec.lean | 10 ++- src/Init/GrindInstances/Ring/Fin.lean | 10 ++- src/Init/GrindInstances/Ring/Int.lean | 6 +- src/Init/GrindInstances/Ring/Nat.lean | 6 +- src/Init/GrindInstances/Ring/SInt.lean | 14 +-- src/Init/GrindInstances/Ring/UInt.lean | 10 ++- src/Init/GrindInstances/ToInt.lean | 20 +++-- src/Init/Guard.lean | 8 +- src/Init/Hints.lean | 4 +- src/Init/Internal.lean | 4 +- src/Init/Internal/Order.lean | 8 +- src/Init/Internal/Order/Basic.lean | 8 +- src/Init/Internal/Order/Lemmas.lean | 10 ++- src/Init/Internal/Order/Tactic.lean | 4 +- src/Init/MacroTrace.lean | 6 +- src/Init/Meta.lean | 16 ++-- src/Init/MetaTypes.lean | 4 +- src/Init/Notation.lean | 4 +- src/Init/NotationExtra.lean | 12 +-- src/Init/Omega.lean | 12 +-- src/Init/Omega/Coeffs.lean | 4 +- src/Init/Omega/Constraint.lean | 6 +- src/Init/Omega/Int.lean | 6 +- src/Init/Omega/IntList.lean | 8 +- src/Init/Omega/LinearCombo.lean | 6 +- src/Init/Omega/Logic.lean | 4 +- src/Init/Prelude.lean | 6 +- src/Init/PropLemmas.lean | 6 +- src/Init/RCases.lean | 6 +- src/Init/ShareCommon.lean | 6 +- src/Init/SimpLemmas.lean | 4 +- src/Init/Simproc.lean | 4 +- src/Init/SizeOf.lean | 4 +- src/Init/SizeOfLemmas.lean | 10 ++- src/Init/Syntax.lean | 4 +- src/Init/System.lean | 12 +-- src/Init/System/FilePath.lean | 6 +- src/Init/System/IO.lean | 12 +-- src/Init/System/IOError.lean | 4 +- src/Init/System/Mutex.lean | 6 +- src/Init/System/Platform.lean | 6 +- src/Init/System/Promise.lean | 4 +- src/Init/System/ST.lean | 8 +- src/Init/System/Uri.lean | 8 +- src/Init/Tactics.lean | 4 +- src/Init/TacticsExtra.lean | 6 +- src/Init/Task.lean | 6 +- src/Init/Try.lean | 4 +- src/Init/Util.lean | 6 +- src/Init/WF.lean | 8 +- src/Init/WFTactics.lean | 8 +- src/Init/While.lean | 4 +- src/Lean/Elab/BuiltinCommand.lean | 11 +-- src/Lean/Elab/Command.lean | 3 +- src/Lean/Elab/DeclModifiers.lean | 61 +++++++------ src/Lean/Elab/Declaration.lean | 29 +++--- src/Lean/Elab/Import.lean | 4 - src/Lean/Elab/MutualDef.lean | 5 +- src/Lean/Elab/ParseImportsFast.lean | 6 +- src/Lean/Parser/Command.lean | 5 +- src/Lean/Parser/Module.lean | 4 +- .../Server/Completion/ImportCompletion.lean | 2 +- .../Server/FileWorker/RequestHandling.lean | 2 +- tests/pkg/module/Module.lean | 16 ++-- tests/pkg/module/Module/Basic.lean | 50 +++++------ tests/pkg/module/Module/Imported.lean | 2 +- tests/pkg/module/Module/ImportedAll.lean | 8 +- .../Module/ImportedAllPrivateImported.lean | 2 +- .../module/Module/ImportedImportedAll.lean | 2 +- .../Module/ImportedPrivateImported.lean | 2 +- tests/pkg/module/Module/NonModule.lean | 4 +- tests/pkg/module/Module/PrivateImported.lean | 8 +- 410 files changed, 2193 insertions(+), 1406 deletions(-) diff --git a/src/Init/BinderNameHint.lean b/src/Init/BinderNameHint.lean index d04722db3d..58baa3c948 100644 --- a/src/Init/BinderNameHint.lean +++ b/src/Init/BinderNameHint.lean @@ -7,8 +7,10 @@ Authors: Joachim Breitner module prelude -import Init.Prelude -import Init.Tactics +public import Init.Prelude +public import Init.Tactics + +public section set_option linter.unusedVariables false in /-- diff --git a/src/Init/BinderPredicates.lean b/src/Init/BinderPredicates.lean index 8640ea67b2..5a72ae29fd 100644 --- a/src/Init/BinderPredicates.lean +++ b/src/Init/BinderPredicates.lean @@ -6,7 +6,9 @@ Authors: Gabriel Ebner module prelude -import Init.NotationExtra +public import Init.NotationExtra + +public section namespace Lean diff --git a/src/Init/ByCases.lean b/src/Init/ByCases.lean index f7f2036aae..20d9e42583 100644 --- a/src/Init/ByCases.lean +++ b/src/Init/ByCases.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Classical +public import Init.Classical + +public section /-! # by_cases tactic and if-then-else support -/ diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index ddcf37ab85..27ac5fd81d 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.PropLemmas +public import Init.PropLemmas + +public section universe u v diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean index 5daa3973e4..4b22887a36 100644 --- a/src/Init/Coe.lean +++ b/src/Init/Coe.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Prelude -meta import Init.Prelude +public import Init.Prelude +public meta import Init.Prelude + +public section set_option linter.missingDocs true -- keep it documented /-! diff --git a/src/Init/Control.lean b/src/Init/Control.lean index dd3668561a..3e06fc820e 100644 --- a/src/Init/Control.lean +++ b/src/Init/Control.lean @@ -6,13 +6,15 @@ Authors: Leonardo de Moura module prelude -import Init.Control.Basic -import Init.Control.State -import Init.Control.StateRef -import Init.Control.Id -import Init.Control.Except -import Init.Control.Reader -import Init.Control.Option -import Init.Control.Lawful -import Init.Control.StateCps -import Init.Control.ExceptCps +public import Init.Control.Basic +public import Init.Control.State +public import Init.Control.StateRef +public import Init.Control.Id +public import Init.Control.Except +public import Init.Control.Reader +public import Init.Control.Option +public import Init.Control.Lawful +public import Init.Control.StateCps +public import Init.Control.ExceptCps + +public section diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index 987744a1da..4766ef9f6f 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -6,8 +6,10 @@ Author: Leonardo de Moura, Sebastian Ullrich module prelude -import Init.Core -import Init.BinderNameHint +public import Init.Core +public import Init.BinderNameHint + +public section universe u v w diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index 4ebad9a7d9..0fe488b61c 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -import Init.Control.State -import Init.Control.Except -import Init.Data.ToString.Basic +public import Init.Control.State +public import Init.Control.Except +public import Init.Data.ToString.Basic + +public section universe u v namespace EStateM diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 1d136ab841..af5b65e984 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -8,9 +8,11 @@ The Except monad transformer. module prelude -import Init.Control.Basic -import Init.Control.Id -import Init.Coe +public import Init.Control.Basic +public import Init.Control.Id +public import Init.Coe + +public section namespace Except variable {ε : Type u} diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean index 461968d12e..b205d27c0e 100644 --- a/src/Init/Control/ExceptCps.lean +++ b/src/Init/Control/ExceptCps.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Control.Lawful.Basic +public import Init.Control.Lawful.Basic + +public section /-! The Exception monad transformer using CPS style. diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean index e19e1a246c..c1d89fbb3c 100644 --- a/src/Init/Control/Id.lean +++ b/src/Init/Control/Id.lean @@ -8,7 +8,9 @@ The identity Monad. module prelude -import Init.Core +public import Init.Core + +public section universe u diff --git a/src/Init/Control/Lawful.lean b/src/Init/Control/Lawful.lean index 004b5edea1..1f2fe2c06a 100644 --- a/src/Init/Control/Lawful.lean +++ b/src/Init/Control/Lawful.lean @@ -6,7 +6,9 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro module prelude -import Init.Control.Lawful.Basic -import Init.Control.Lawful.Instances -import Init.Control.Lawful.Lemmas -import Init.Control.Lawful.MonadLift +public import Init.Control.Lawful.Basic +public import Init.Control.Lawful.Instances +public import Init.Control.Lawful.Lemmas +public import Init.Control.Lawful.MonadLift + +public section diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index 2f24401125..45e1db4553 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -6,9 +6,11 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro module prelude -import Init.Ext -import Init.SimpLemmas -import Init.Meta +public import Init.Ext +public import Init.SimpLemmas +public import Init.Meta + +public section open Function diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean index 45ee782149..df8fc13403 100644 --- a/src/Init/Control/Lawful/Instances.lean +++ b/src/Init/Control/Lawful/Instances.lean @@ -6,11 +6,13 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro module prelude -import Init.Control.Lawful.Basic -import all Init.Control.Except -import all Init.Control.State -import Init.Control.StateRef -import Init.Ext +public import Init.Control.Lawful.Basic +public import all Init.Control.Except +public import all Init.Control.State +public import Init.Control.StateRef +public import Init.Ext + +public section open Function diff --git a/src/Init/Control/Lawful/Lemmas.lean b/src/Init/Control/Lawful/Lemmas.lean index 90fefe337b..9de277d339 100644 --- a/src/Init/Control/Lawful/Lemmas.lean +++ b/src/Init/Control/Lawful/Lemmas.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Control.Lawful.Basic -import Init.RCases -import Init.ByCases +public import Init.Control.Lawful.Basic +public import Init.RCases +public import Init.ByCases + +public section -- Mapping by a function with a left inverse is injective. theorem map_inj_of_left_inverse [Functor m] [LawfulFunctor m] {f : α → β} diff --git a/src/Init/Control/Lawful/MonadLift.lean b/src/Init/Control/Lawful/MonadLift.lean index 19640c7dca..42811f6638 100644 --- a/src/Init/Control/Lawful/MonadLift.lean +++ b/src/Init/Control/Lawful/MonadLift.lean @@ -6,6 +6,8 @@ Authors: Paul Reichert module prelude -import Init.Control.Lawful.MonadLift.Basic -import Init.Control.Lawful.MonadLift.Lemmas -import Init.Control.Lawful.MonadLift.Instances +public import Init.Control.Lawful.MonadLift.Basic +public import Init.Control.Lawful.MonadLift.Lemmas +public import Init.Control.Lawful.MonadLift.Instances + +public section diff --git a/src/Init/Control/Lawful/MonadLift/Basic.lean b/src/Init/Control/Lawful/MonadLift/Basic.lean index 374cfad929..60cdcb428c 100644 --- a/src/Init/Control/Lawful/MonadLift/Basic.lean +++ b/src/Init/Control/Lawful/MonadLift/Basic.lean @@ -6,7 +6,9 @@ Authors: Quang Dao module prelude -import Init.Control.Basic +public import Init.Control.Basic + +public section /-! # LawfulMonadLift and LawfulMonadLiftT diff --git a/src/Init/Control/Lawful/MonadLift/Instances.lean b/src/Init/Control/Lawful/MonadLift/Instances.lean index ec3e75b441..79a38d8251 100644 --- a/src/Init/Control/Lawful/MonadLift/Instances.lean +++ b/src/Init/Control/Lawful/MonadLift/Instances.lean @@ -6,14 +6,16 @@ Authors: Quang Dao, Paul Reichert module prelude -import all Init.Control.Option -import all Init.Control.Except -import all Init.Control.ExceptCps -import all Init.Control.StateRef -import all Init.Control.StateCps -import all Init.Control.Id -import Init.Control.Lawful.MonadLift.Lemmas -import Init.Control.Lawful.Instances +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.Lawful.MonadLift.Lemmas +public import Init.Control.Lawful.Instances + +public section universe u v w x diff --git a/src/Init/Control/Lawful/MonadLift/Lemmas.lean b/src/Init/Control/Lawful/MonadLift/Lemmas.lean index da2208eefa..cd617a3621 100644 --- a/src/Init/Control/Lawful/MonadLift/Lemmas.lean +++ b/src/Init/Control/Lawful/MonadLift/Lemmas.lean @@ -6,8 +6,10 @@ Authors: Quang Dao module prelude -import Init.Control.Lawful.Basic -import Init.Control.Lawful.MonadLift.Basic +public import Init.Control.Lawful.Basic +public import Init.Control.Lawful.MonadLift.Basic + +public section universe u v w diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index f211be0498..9155ce4c49 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura, Sebastian Ullrich module prelude -import Init.Data.Option.Basic -import Init.Control.Basic -import Init.Control.Except +public import Init.Data.Option.Basic +public import Init.Control.Basic +public import Init.Control.Except + +public section set_option linter.missingDocs true diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean index ed59cb61ef..e01c7c3f97 100644 --- a/src/Init/Control/Reader.lean +++ b/src/Init/Control/Reader.lean @@ -8,9 +8,11 @@ The Reader monad transformer for passing immutable State. module prelude -import Init.Control.Basic -import Init.Control.Id -import Init.Control.Except +public import Init.Control.Basic +public import Init.Control.Id +public import Init.Control.Except + +public section set_option linter.missingDocs true diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index 78ea0330ca..efa8871174 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -8,9 +8,11 @@ The State monad transformer. module prelude -import Init.Control.Basic -import Init.Control.Id -import Init.Control.Except +public import Init.Control.Basic +public import Init.Control.Id +public import Init.Control.Except + +public section set_option linter.missingDocs true diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean index a111dce891..db8b57a9dd 100644 --- a/src/Init/Control/StateCps.lean +++ b/src/Init/Control/StateCps.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Control.Lawful.Basic +public import Init.Control.Lawful.Basic + +public section set_option linter.missingDocs true diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean index 3cb89aa68f..86d99181ef 100644 --- a/src/Init/Control/StateRef.lean +++ b/src/Init/Control/StateRef.lean @@ -8,7 +8,9 @@ The State monad transformer using IO references. module prelude -import Init.System.ST +public import Init.System.ST + +public section set_option linter.missingDocs true diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 49dde3c540..9934d1653e 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -8,8 +8,10 @@ Notation for operators defined at Prelude.lean module prelude -import Init.Tactics -meta import Init.Meta +public import Init.Tactics +public meta import Init.Meta + +public section namespace Lean.Parser.Tactic.Conv diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 864b7280e0..e2974f8122 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -8,8 +8,10 @@ notation, basic datatypes and type classes module prelude -meta import Init.Prelude -import Init.SizeOf +public meta import Init.Prelude +public import Init.SizeOf + +public section set_option linter.missingDocs true -- keep it documented @[expose] section diff --git a/src/Init/Data.lean b/src/Init/Data.lean index 6fd13e88d4..5b9d6fd6ec 100644 --- a/src/Init/Data.lean +++ b/src/Init/Data.lean @@ -6,46 +6,48 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Basic -import Init.Data.Nat -import Init.Data.Bool -import Init.Data.BitVec -import Init.Data.Cast -import Init.Data.Char -import Init.Data.String -import Init.Data.List -import Init.Data.Int -import Init.Data.Array -import Init.Data.Array.Subarray.Split -import Init.Data.ByteArray -import Init.Data.FloatArray -import Init.Data.Fin -import Init.Data.UInt -import Init.Data.SInt -import Init.Data.Float -import Init.Data.Float32 -import Init.Data.Option -import Init.Data.Ord -import Init.Data.Random -import Init.Data.ToString -import Init.Data.Range -import Init.Data.Hashable -import Init.Data.OfScientific -import Init.Data.Format -import Init.Data.Stream -import Init.Data.Prod -import Init.Data.AC -import Init.Data.Queue -import Init.Data.Sum -import Init.Data.BEq -import Init.Data.Subtype -import Init.Data.ULift -import Init.Data.PLift -import Init.Data.Zero -import Init.Data.NeZero -import Init.Data.Function -import Init.Data.RArray -import Init.Data.Vector -import Init.Data.Iterators -import Init.Data.Range.Polymorphic -import Init.Data.Slice +public import Init.Data.Basic +public import Init.Data.Nat +public import Init.Data.Bool +public import Init.Data.BitVec +public import Init.Data.Cast +public import Init.Data.Char +public import Init.Data.String +public import Init.Data.List +public import Init.Data.Int +public import Init.Data.Array +public import Init.Data.Array.Subarray.Split +public import Init.Data.ByteArray +public import Init.Data.FloatArray +public import Init.Data.Fin +public import Init.Data.UInt +public import Init.Data.SInt +public import Init.Data.Float +public import Init.Data.Float32 +public import Init.Data.Option +public import Init.Data.Ord +public import Init.Data.Random +public import Init.Data.ToString +public import Init.Data.Range +public import Init.Data.Hashable +public import Init.Data.OfScientific +public import Init.Data.Format +public import Init.Data.Stream +public import Init.Data.Prod +public import Init.Data.AC +public import Init.Data.Queue +public import Init.Data.Sum +public import Init.Data.BEq +public import Init.Data.Subtype +public import Init.Data.ULift +public import Init.Data.PLift +public import Init.Data.Zero +public import Init.Data.NeZero +public import Init.Data.Function +public import Init.Data.RArray +public import Init.Data.Vector +public import Init.Data.Iterators +public import Init.Data.Range.Polymorphic +public import Init.Data.Slice + +public section diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean index aa9441fe24..b71d487f40 100644 --- a/src/Init/Data/AC.lean +++ b/src/Init/Data/AC.lean @@ -7,8 +7,10 @@ Authors: Dany Fabian module prelude -import Init.Classical -import Init.ByCases +public import Init.Classical +public import Init.ByCases + +public section namespace Lean.Data.AC inductive Expr diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean index 2b3259b596..0afae8e992 100644 --- a/src/Init/Data/Array.lean +++ b/src/Init/Data/Array.lean @@ -6,27 +6,29 @@ Authors: Gabriel Ebner module prelude -import Init.Data.Array.Basic -import Init.Data.Array.QSort -import Init.Data.Array.BinSearch -import Init.Data.Array.InsertionSort -import Init.Data.Array.DecidableEq -import Init.Data.Array.Mem -import Init.Data.Array.Attach -import Init.Data.Array.BasicAux -import Init.Data.Array.Lemmas -import Init.Data.Array.TakeDrop -import Init.Data.Array.Bootstrap -import Init.Data.Array.GetLit -import Init.Data.Array.MapIdx -import Init.Data.Array.Set -import Init.Data.Array.Monadic -import Init.Data.Array.FinRange -import Init.Data.Array.Perm -import Init.Data.Array.Find -import Init.Data.Array.Lex -import Init.Data.Array.Range -import Init.Data.Array.Erase -import Init.Data.Array.Zip -import Init.Data.Array.InsertIdx -import Init.Data.Array.Extract +public import Init.Data.Array.Basic +public import Init.Data.Array.QSort +public import Init.Data.Array.BinSearch +public import Init.Data.Array.InsertionSort +public import Init.Data.Array.DecidableEq +public import Init.Data.Array.Mem +public import Init.Data.Array.Attach +public import Init.Data.Array.BasicAux +public import Init.Data.Array.Lemmas +public import Init.Data.Array.TakeDrop +public import Init.Data.Array.Bootstrap +public import Init.Data.Array.GetLit +public import Init.Data.Array.MapIdx +public import Init.Data.Array.Set +public import Init.Data.Array.Monadic +public import Init.Data.Array.FinRange +public import Init.Data.Array.Perm +public import Init.Data.Array.Find +public import Init.Data.Array.Lex +public import Init.Data.Array.Range +public import Init.Data.Array.Erase +public import Init.Data.Array.Zip +public import Init.Data.Array.InsertIdx +public import Init.Data.Array.Extract + +public section diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean index 65f2cc9c40..a79c2a9cf2 100644 --- a/src/Init/Data/Array/Attach.lean +++ b/src/Init/Data/Array/Attach.lean @@ -6,10 +6,12 @@ Authors: Joachim Breitner, Mario Carneiro module prelude -import Init.Data.Array.Mem -import Init.Data.Array.Lemmas -import Init.Data.Array.Count -import all Init.Data.List.Attach +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 section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 4491c7de89..17b5c35337 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -6,15 +6,17 @@ Authors: Leonardo de Moura module prelude -import Init.WFTactics -import Init.Data.Nat.Basic -import Init.Data.Fin.Basic -import Init.Data.UInt.BasicAux -import Init.Data.Repr -import Init.Data.ToString.Basic -import Init.GetElem -import all Init.Data.List.ToArrayImpl -import all Init.Data.Array.Set +public import Init.WFTactics +public import Init.Data.Nat.Basic +public import Init.Data.Fin.Basic +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 section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean index 9f24e79ee5..6c96cdaddd 100644 --- a/src/Init/Data/Array/BasicAux.lean +++ b/src/Init/Data/Array/BasicAux.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -import all Init.Data.Array.Basic -import Init.Data.Nat.Linear -import Init.NotationExtra +public import all Init.Data.Array.Basic +public import Init.Data.Nat.Linear +public import Init.NotationExtra + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean index ed96e55932..4c9604ade1 100644 --- a/src/Init/Data/Array/BinSearch.lean +++ b/src/Init/Data/Array/BinSearch.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Array.Basic -import Init.Data.Int.DivMod.Lemmas -import Init.Omega +public import Init.Data.Array.Basic +public import Init.Data.Int.DivMod.Lemmas +public import Init.Omega + +public section universe u v set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index 0d4c41374d..479a4054dc 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -7,8 +7,10 @@ Authors: Mario Carneiro module prelude -import Init.Data.List.TakeDrop -import all Init.Data.Array.Basic +public import Init.Data.List.TakeDrop +public import all Init.Data.Array.Basic + +public section /-! ## Bootstrapping theorems about arrays diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean index 453af51aa4..5d1b61a93e 100644 --- a/src/Init/Data/Array/Count.lean +++ b/src/Init/Data/Array/Count.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Basic -import Init.Data.Array.Lemmas -import Init.Data.List.Nat.Count +public import all Init.Data.Array.Basic +public import Init.Data.Array.Lemmas +public import Init.Data.List.Nat.Count + +public section /-! # Lemmas about `Array.countP` and `Array.count`. diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index e2074a743c..fd96598073 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura module prelude -import all Init.Data.Array.Basic -import Init.Data.BEq -import Init.Data.List.Nat.BEq -import Init.ByCases +public import all Init.Data.Array.Basic +public import Init.Data.BEq +public import Init.Data.List.Nat.BEq +public import Init.ByCases + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean index d66161a8e5..9f9a4f4e6d 100644 --- a/src/Init/Data/Array/Erase.lean +++ b/src/Init/Data/Array/Erase.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Basic -import Init.Data.Array.Lemmas -import Init.Data.List.Nat.Erase -import Init.Data.List.Nat.Basic +public 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 + +public section /-! # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`. diff --git a/src/Init/Data/Array/Extract.lean b/src/Init/Data/Array/Extract.lean index c69a89dee1..0e9c40b297 100644 --- a/src/Init/Data/Array/Extract.lean +++ b/src/Init/Data/Array/Extract.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Array.Lemmas -import Init.Data.List.Nat.TakeDrop +public import Init.Data.Array.Lemmas +public import Init.Data.List.Nat.TakeDrop + +public section /-! # Lemmas about `Array.extract` diff --git a/src/Init/Data/Array/FinRange.lean b/src/Init/Data/Array/FinRange.lean index 1bce783fc9..93da71ebbf 100644 --- a/src/Init/Data/Array/FinRange.lean +++ b/src/Init/Data/Array/FinRange.lean @@ -6,8 +6,10 @@ Authors: François G. Dorais module prelude -import Init.Data.List.FinRange -import Init.Data.Array.OfFn +public import Init.Data.List.FinRange +public import Init.Data.Array.OfFn + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index 5fb59532ea..4e43f3e019 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean @@ -6,11 +6,13 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Nat.Find -import all Init.Data.Array.Basic -import Init.Data.Array.Lemmas -import Init.Data.Array.Attach -import Init.Data.Array.Range +public import Init.Data.List.Nat.Find +public import all Init.Data.Array.Basic +public import Init.Data.Array.Lemmas +public import Init.Data.Array.Attach +public import Init.Data.Array.Range + +public section /-! # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`. diff --git a/src/Init/Data/Array/GetLit.lean b/src/Init/Data/Array/GetLit.lean index f020cad254..855d4f2d58 100644 --- a/src/Init/Data/Array/GetLit.lean +++ b/src/Init/Data/Array/GetLit.lean @@ -7,7 +7,9 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Array.Basic +public import Init.Data.Array.Basic + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/InsertIdx.lean b/src/Init/Data/Array/InsertIdx.lean index 2c8832b7e4..68cbc45673 100644 --- a/src/Init/Data/Array/InsertIdx.lean +++ b/src/Init/Data/Array/InsertIdx.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Array.Lemmas -import Init.Data.List.Nat.InsertIdx +public import Init.Data.Array.Lemmas +public import Init.Data.List.Nat.InsertIdx + +public section /-! # insertIdx diff --git a/src/Init/Data/Array/InsertionSort.lean b/src/Init/Data/Array/InsertionSort.lean index 9b2dd6c950..656f223e47 100644 --- a/src/Init/Data/Array/InsertionSort.lean +++ b/src/Init/Data/Array/InsertionSort.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Array.Basic +public import Init.Data.Array.Basic + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index c015042f86..37d4565acc 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -6,21 +6,23 @@ Authors: Mario Carneiro, Kim Morrison module prelude -import Init.Data.Nat.Lemmas -import Init.Data.List.Range -import all Init.Data.List.Control -import Init.Data.List.Nat.TakeDrop -import Init.Data.List.Nat.Modify -import Init.Data.List.Nat.Basic -import Init.Data.List.Monadic -import Init.Data.List.OfFn -import all Init.Data.Array.Bootstrap -import Init.Data.Array.Mem -import Init.Data.Array.DecidableEq -import Init.Data.Array.Lex.Basic -import Init.Data.Range.Lemmas -import Init.TacticsExtra -import Init.Data.List.ToArray +public import Init.Data.Nat.Lemmas +public import Init.Data.List.Range +public import all Init.Data.List.Control +public import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Nat.Modify +public import Init.Data.List.Nat.Basic +public import Init.Data.List.Monadic +public import Init.Data.List.OfFn +public import all Init.Data.Array.Bootstrap +public import Init.Data.Array.Mem +public import Init.Data.Array.DecidableEq +public import Init.Data.Array.Lex.Basic +public import Init.Data.Range.Lemmas +public import Init.TacticsExtra +public import Init.Data.List.ToArray + +public section /-! ## Theorems about `Array`. diff --git a/src/Init/Data/Array/Lex.lean b/src/Init/Data/Array/Lex.lean index 4bf9e0f655..ce0a5f7f8d 100644 --- a/src/Init/Data/Array/Lex.lean +++ b/src/Init/Data/Array/Lex.lean @@ -6,5 +6,7 @@ Author: Kim Morrison module prelude -import Init.Data.Array.Lex.Basic -import Init.Data.Array.Lex.Lemmas +public import Init.Data.Array.Lex.Basic +public import Init.Data.Array.Lex.Lemmas + +public section diff --git a/src/Init/Data/Array/Lex/Basic.lean b/src/Init/Data/Array/Lex/Basic.lean index 0d287555d7..7277a44b5a 100644 --- a/src/Init/Data/Array/Lex/Basic.lean +++ b/src/Init/Data/Array/Lex/Basic.lean @@ -6,9 +6,11 @@ Author: Kim Morrison module prelude -import Init.Data.Array.Basic -import Init.Data.Nat.Lemmas -import Init.Data.Range +public import Init.Data.Array.Basic +public import Init.Data.Nat.Lemmas +public import Init.Data.Range + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index 3e5b6d48a6..7aa497e173 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -6,9 +6,11 @@ Author: Kim Morrison module prelude -import all Init.Data.Array.Lex.Basic -import Init.Data.Array.Lemmas -import Init.Data.List.Lex +public import all Init.Data.Array.Lex.Basic +public import Init.Data.Array.Lemmas +public import Init.Data.List.Lex + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index b6683792af..f425d9aa94 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 -import all Init.Data.Array.Basic -import Init.Data.Array.Lemmas -import Init.Data.Array.Attach -import Init.Data.Array.OfFn -import all Init.Data.List.MapIdx +public 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 section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean index b66f520dbd..736a8558be 100644 --- a/src/Init/Data/Array/Mem.lean +++ b/src/Init/Data/Array/Mem.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura, Joachim Breitner module prelude -import Init.Data.Array.Basic -import Init.Data.Nat.Linear -import Init.Data.List.BasicAux +public import Init.Data.Array.Basic +public import Init.Data.Nat.Linear +public import Init.Data.List.BasicAux + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean index 0dabd48a9a..e8e8c25e81 100644 --- a/src/Init/Data/Array/Monadic.lean +++ b/src/Init/Data/Array/Monadic.lean @@ -6,11 +6,13 @@ Authors: Kim Morrison module prelude -import all Init.Data.List.Control -import all Init.Data.Array.Basic -import Init.Data.Array.Lemmas -import Init.Data.Array.Attach -import Init.Data.List.Monadic +public import all Init.Data.List.Control +public import all Init.Data.Array.Basic +public import Init.Data.Array.Lemmas +public import Init.Data.Array.Attach +public import Init.Data.List.Monadic + +public section /-! # Lemmas about `Array.forIn'` and `Array.forIn`. diff --git a/src/Init/Data/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean index 39adb3343b..8d8238b9a2 100644 --- a/src/Init/Data/Array/OfFn.lean +++ b/src/Init/Data/Array/OfFn.lean @@ -6,11 +6,13 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Basic -import Init.Data.Array.Lemmas -import Init.Data.Array.Monadic -import Init.Data.List.OfFn -import Init.Data.List.FinRange +public import all Init.Data.Array.Basic +public import Init.Data.Array.Lemmas +public import Init.Data.Array.Monadic +public import Init.Data.List.OfFn +public import Init.Data.List.FinRange + +public section /-! # Theorems about `Array.ofFn` diff --git a/src/Init/Data/Array/Perm.lean b/src/Init/Data/Array/Perm.lean index 7d3df9b3ac..9e8a4d922b 100644 --- a/src/Init/Data/Array/Perm.lean +++ b/src/Init/Data/Array/Perm.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Nat.Perm -import all Init.Data.Array.Basic -import Init.Data.Array.Lemmas +public import Init.Data.List.Nat.Perm +public import all Init.Data.Array.Basic +public import Init.Data.Array.Lemmas + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean index cbefecee76..8919cb66ca 100644 --- a/src/Init/Data/Array/QSort.lean +++ b/src/Init/Data/Array/QSort.lean @@ -6,4 +6,6 @@ Authors: Kim Morrison module prelude -import Init.Data.Array.QSort.Basic +public import Init.Data.Array.QSort.Basic + +public section diff --git a/src/Init/Data/Array/QSort/Basic.lean b/src/Init/Data/Array/QSort/Basic.lean index 070aaa9eb2..863b46b78b 100644 --- a/src/Init/Data/Array/QSort/Basic.lean +++ b/src/Init/Data/Array/QSort/Basic.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Vector.Basic -import Init.Data.Ord +public import Init.Data.Vector.Basic +public import Init.Data.Ord + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. -- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc. diff --git a/src/Init/Data/Array/Range.lean b/src/Init/Data/Array/Range.lean index 4d4bbcfb6a..16b05f1400 100644 --- a/src/Init/Data/Array/Range.lean +++ b/src/Init/Data/Array/Range.lean @@ -6,12 +6,14 @@ Authors: Kim Morrison module prelude -import Init.Data.Array.Lemmas -import all Init.Data.Array.Basic -import all Init.Data.Array.OfFn -import Init.Data.Array.MapIdx -import Init.Data.Array.Zip -import Init.Data.List.Nat.Range +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.MapIdx +public import Init.Data.Array.Zip +public import Init.Data.List.Nat.Range + +public section /-! # Lemmas about `Array.range'`, `Array.range`, and `Array.zipIdx` diff --git a/src/Init/Data/Array/Set.lean b/src/Init/Data/Array/Set.lean index 468e483b74..59b1dbf31a 100644 --- a/src/Init/Data/Array/Set.lean +++ b/src/Init/Data/Array/Set.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Tactics +public import Init.Tactics + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 0cfc5f89a3..c9162ce856 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Array.Basic -import Init.Data.Slice.Basic +public import Init.Data.Array.Basic +public import Init.Data.Slice.Basic + +public section set_option linter.indexVariables true -- Enforce naming conventions for index variables. set_option linter.missingDocs true diff --git a/src/Init/Data/Array/Subarray/Split.lean b/src/Init/Data/Array/Subarray/Split.lean index 331d4cbd8c..61cd40dd65 100644 --- a/src/Init/Data/Array/Subarray/Split.lean +++ b/src/Init/Data/Array/Subarray/Split.lean @@ -7,9 +7,11 @@ Authors: David Thrane Christiansen module prelude -import Init.Data.Array.Basic -import all Init.Data.Array.Subarray -import Init.Omega +public import Init.Data.Array.Basic +public import all Init.Data.Array.Subarray +public import Init.Omega + +public section /- This module contains splitting operations on subarrays that crucially rely on `omega` for proof diff --git a/src/Init/Data/Array/TakeDrop.lean b/src/Init/Data/Array/TakeDrop.lean index de1db6899d..805d7d9dd7 100644 --- a/src/Init/Data/Array/TakeDrop.lean +++ b/src/Init/Data/Array/TakeDrop.lean @@ -6,9 +6,11 @@ Authors: Markus Himmel module prelude -import all Init.Data.Array.Basic -import Init.Data.Array.Lemmas -import Init.Data.List.Nat.TakeDrop +public import all Init.Data.Array.Basic +public import Init.Data.Array.Lemmas +public import Init.Data.List.Nat.TakeDrop + +public section /-! These lemmas are used in the internals of HashMap. diff --git a/src/Init/Data/Array/Zip.lean b/src/Init/Data/Array/Zip.lean index cd60825c4d..679bf1d557 100644 --- a/src/Init/Data/Array/Zip.lean +++ b/src/Init/Data/Array/Zip.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Basic -import Init.Data.Array.TakeDrop -import Init.Data.List.Zip +public import all Init.Data.Array.Basic +public import Init.Data.Array.TakeDrop +public import Init.Data.List.Zip + +public section /-! # Lemmas about `Array.zip`, `Array.zipWith`, `Array.zipWithAll`, and `Array.unzip`. diff --git a/src/Init/Data/BEq.lean b/src/Init/Data/BEq.lean index 2cb394352a..822a71dc45 100644 --- a/src/Init/Data/BEq.lean +++ b/src/Init/Data/BEq.lean @@ -6,7 +6,9 @@ Authors: Mario Carneiro, Markus Himmel module prelude -import Init.Data.Bool +public import Init.Data.Bool + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/Basic.lean b/src/Init/Data/Basic.lean index 5a29c6859b..418cf55401 100644 --- a/src/Init/Data/Basic.lean +++ b/src/Init/Data/Basic.lean @@ -6,13 +6,15 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Nat.Basic -import Init.Data.Fin.Basic -import Init.Data.List.Basic -import Init.Data.Char.Basic -import Init.Data.String.Basic -import Init.Data.Option.Basic -import Init.Data.UInt -import Init.Data.Repr -import Init.Data.ToString.Basic -import Init.Data.String.Extra +public import Init.Data.Nat.Basic +public import Init.Data.Fin.Basic +public import Init.Data.List.Basic +public import Init.Data.Char.Basic +public import Init.Data.String.Basic +public import Init.Data.Option.Basic +public import Init.Data.UInt +public import Init.Data.Repr +public import Init.Data.ToString.Basic +public import Init.Data.String.Extra + +public section diff --git a/src/Init/Data/BitVec.lean b/src/Init/Data/BitVec.lean index 4f22797680..35d77c06f6 100644 --- a/src/Init/Data/BitVec.lean +++ b/src/Init/Data/BitVec.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import Init.Data.BitVec.BasicAux -import Init.Data.BitVec.Basic -import Init.Data.BitVec.Bootstrap -import Init.Data.BitVec.Bitblast -import Init.Data.BitVec.Decidable -import Init.Data.BitVec.Lemmas -import Init.Data.BitVec.Folds +public import Init.Data.BitVec.BasicAux +public import Init.Data.BitVec.Basic +public import Init.Data.BitVec.Bootstrap +public import Init.Data.BitVec.Bitblast +public import Init.Data.BitVec.Decidable +public import Init.Data.BitVec.Lemmas +public import Init.Data.BitVec.Folds + +public section diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 410eca04d0..2c499eac38 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -6,11 +6,13 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex module prelude -import Init.Data.Fin.Basic -import Init.Data.Nat.Bitwise.Lemmas -import Init.Data.Nat.Power2 -import Init.Data.Int.Bitwise -import Init.Data.BitVec.BasicAux +public import Init.Data.Fin.Basic +public import Init.Data.Nat.Bitwise.Lemmas +public import Init.Data.Nat.Power2 +public import Init.Data.Int.Bitwise +public import Init.Data.BitVec.BasicAux + +public section /-! We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over diff --git a/src/Init/Data/BitVec/BasicAux.lean b/src/Init/Data/BitVec/BasicAux.lean index d35ce7d599..d24139bf98 100644 --- a/src/Init/Data/BitVec/BasicAux.lean +++ b/src/Init/Data/BitVec/BasicAux.lean @@ -6,7 +6,9 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex module prelude -import Init.Data.Fin.Basic +public import Init.Data.Fin.Basic + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 2582562152..f566983bac 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -6,14 +6,16 @@ Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat module prelude -import all Init.Data.Nat.Bitwise.Basic -import Init.Data.Nat.Mod -import all Init.Data.Int.DivMod -import Init.Data.Int.LemmasAux -import all Init.Data.BitVec.Basic -import Init.Data.BitVec.Decidable -import Init.Data.BitVec.Lemmas -import Init.Data.BitVec.Folds +public 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.LemmasAux +public import all Init.Data.BitVec.Basic +public import Init.Data.BitVec.Decidable +public import Init.Data.BitVec.Lemmas +public import Init.Data.BitVec.Folds + +public section /-! # Bit blasting of bitvectors diff --git a/src/Init/Data/BitVec/Bootstrap.lean b/src/Init/Data/BitVec/Bootstrap.lean index f9e25df016..44ba6bfe42 100644 --- a/src/Init/Data/BitVec/Bootstrap.lean +++ b/src/Init/Data/BitVec/Bootstrap.lean @@ -6,7 +6,9 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B module prelude -import all Init.Data.BitVec.Basic +public import all Init.Data.BitVec.Basic + +public section namespace BitVec diff --git a/src/Init/Data/BitVec/Decidable.lean b/src/Init/Data/BitVec/Decidable.lean index 5283380e09..f956d8b1f3 100644 --- a/src/Init/Data/BitVec/Decidable.lean +++ b/src/Init/Data/BitVec/Decidable.lean @@ -7,7 +7,9 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B module prelude -import Init.Data.BitVec.Bootstrap +public import Init.Data.BitVec.Bootstrap + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/BitVec/Folds.lean b/src/Init/Data/BitVec/Folds.lean index d1007a318c..39d4d53914 100644 --- a/src/Init/Data/BitVec/Folds.lean +++ b/src/Init/Data/BitVec/Folds.lean @@ -6,10 +6,12 @@ Authors: Joe Hendrix, Harun Khan module prelude -import all Init.Data.BitVec.Basic -import Init.Data.BitVec.Lemmas -import Init.Data.Nat.Lemmas -import Init.Data.Fin.Iterate +public import all Init.Data.BitVec.Basic +public import Init.Data.BitVec.Lemmas +public import Init.Data.Nat.Lemmas +public import Init.Data.Fin.Iterate + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index d8e5783875..1ce55ff178 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -6,19 +6,21 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B module prelude -import Init.Data.Bool -import all Init.Data.BitVec.Basic -import all Init.Data.BitVec.BasicAux -import Init.Data.Fin.Lemmas -import Init.Data.Nat.Lemmas -import Init.Data.Nat.Div.Lemmas -import Init.Data.Nat.Mod -import Init.Data.Nat.Div.Lemmas -import Init.Data.Int.Bitwise.Lemmas -import Init.Data.Int.LemmasAux -import Init.Data.Int.Pow -import Init.Data.Int.LemmasAux -import Init.Data.BitVec.Bootstrap +public import Init.Data.Bool +public import all Init.Data.BitVec.Basic +public 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 +public import Init.Data.Nat.Mod +public import Init.Data.Nat.Div.Lemmas +public import Init.Data.Int.Bitwise.Lemmas +public import Init.Data.Int.LemmasAux +public import Init.Data.Int.Pow +public import Init.Data.Int.LemmasAux +public import Init.Data.BitVec.Bootstrap + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index af696ed4c1..a68998f55a 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -6,7 +6,9 @@ Authors: F. G. Dorais module prelude -import Init.NotationExtra +public import Init.NotationExtra + +public section namespace Bool diff --git a/src/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean index 2e513d63f4..2a6f6e45bd 100644 --- a/src/Init/Data/ByteArray.lean +++ b/src/Init/Data/ByteArray.lean @@ -6,4 +6,6 @@ Author: Leonardo de Moura module prelude -import Init.Data.ByteArray.Basic +public import Init.Data.ByteArray.Basic + +public section diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index c19bf11c21..df729f2de4 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -6,10 +6,12 @@ Author: Leonardo de Moura module prelude -import Init.Data.Array.Basic -import Init.Data.UInt.Basic -import all Init.Data.UInt.BasicAux -import Init.Data.Option.Basic +public import Init.Data.Array.Basic +public import Init.Data.UInt.Basic +public import all Init.Data.UInt.BasicAux +public import Init.Data.Option.Basic + +public section universe u structure ByteArray where diff --git a/src/Init/Data/Cast.lean b/src/Init/Data/Cast.lean index 037b7c1da1..7cde123384 100644 --- a/src/Init/Data/Cast.lean +++ b/src/Init/Data/Cast.lean @@ -6,7 +6,9 @@ Authors: Mario Carneiro, Gabriel Ebner module prelude -import Init.Coe +public import Init.Coe + +public section /-! # `NatCast` diff --git a/src/Init/Data/Char.lean b/src/Init/Data/Char.lean index 8b890f93e8..4b17d13e24 100644 --- a/src/Init/Data/Char.lean +++ b/src/Init/Data/Char.lean @@ -6,5 +6,7 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Char.Basic -import Init.Data.Char.Lemmas +public import Init.Data.Char.Basic +public import Init.Data.Char.Lemmas + +public section diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean index 1e89f580f6..c64fa95118 100644 --- a/src/Init/Data/Char/Basic.lean +++ b/src/Init/Data/Char/Basic.lean @@ -6,7 +6,9 @@ Author: Leonardo de Moura module prelude -import Init.Data.UInt.BasicAux +public import Init.Data.UInt.BasicAux + +public section /-- Determines if the given integer is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value). diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean index ea7a7336de..886da02e8a 100644 --- a/src/Init/Data/Char/Lemmas.lean +++ b/src/Init/Data/Char/Lemmas.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import all Init.Data.Char.Basic -import Init.Data.UInt.Lemmas +public import all Init.Data.Char.Basic +public import Init.Data.UInt.Lemmas + +public section namespace Char diff --git a/src/Init/Data/Fin.lean b/src/Init/Data/Fin.lean index 172db74a4a..014a77e9ab 100644 --- a/src/Init/Data/Fin.lean +++ b/src/Init/Data/Fin.lean @@ -6,8 +6,10 @@ Author: Leonardo de Moura module prelude -import Init.Data.Fin.Basic -import Init.Data.Fin.Log2 -import Init.Data.Fin.Iterate -import Init.Data.Fin.Fold -import Init.Data.Fin.Lemmas +public import Init.Data.Fin.Basic +public import Init.Data.Fin.Log2 +public import Init.Data.Fin.Iterate +public import Init.Data.Fin.Fold +public import Init.Data.Fin.Lemmas + +public section diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index 180d6b1d82..c45213dd09 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -6,7 +6,9 @@ Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro module prelude -import Init.Data.Nat.Bitwise.Basic +public import Init.Data.Nat.Bitwise.Basic + +public section @[expose] section diff --git a/src/Init/Data/Fin/Bitwise.lean b/src/Init/Data/Fin/Bitwise.lean index 25c582a5f7..459c349004 100644 --- a/src/Init/Data/Fin/Bitwise.lean +++ b/src/Init/Data/Fin/Bitwise.lean @@ -6,8 +6,10 @@ Authors: Markus Himmel module prelude -import Init.Data.Nat.Bitwise -import Init.Data.Fin.Basic +public import Init.Data.Nat.Bitwise +public import Init.Data.Fin.Basic + +public section namespace Fin diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index 1d85ec132b..cbc69d08a7 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -6,9 +6,11 @@ Authors: François G. Dorais module prelude -import Init.Data.Nat.Linear -import Init.Control.Lawful.Basic -import Init.Data.Fin.Lemmas +public import Init.Data.Nat.Linear +public import Init.Control.Lawful.Basic +public import Init.Data.Fin.Lemmas + +public section namespace Fin diff --git a/src/Init/Data/Fin/Iterate.lean b/src/Init/Data/Fin/Iterate.lean index 880042b9bf..7de6abd4ac 100644 --- a/src/Init/Data/Fin/Iterate.lean +++ b/src/Init/Data/Fin/Iterate.lean @@ -6,8 +6,10 @@ Authors: Joe Hendrix module prelude -import Init.PropLemmas -import Init.Data.Fin.Basic +public import Init.PropLemmas +public import Init.Data.Fin.Basic + +public section namespace Fin diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index c02c70cd1f..a7a1935493 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -6,12 +6,14 @@ Authors: Mario Carneiro, Leonardo de Moura module prelude -import Init.Data.Nat.Lemmas -import Init.Data.Int.DivMod.Lemmas -import Init.Ext -import Init.ByCases -import Init.Conv -import Init.Omega +public import Init.Data.Nat.Lemmas +public import Init.Data.Int.DivMod.Lemmas +public import Init.Ext +public import Init.ByCases +public import Init.Conv +public import Init.Omega + +public section namespace Fin diff --git a/src/Init/Data/Fin/Log2.lean b/src/Init/Data/Fin/Log2.lean index f1cf1aea5c..d96cf0124a 100644 --- a/src/Init/Data/Fin/Log2.lean +++ b/src/Init/Data/Fin/Log2.lean @@ -6,7 +6,9 @@ Authors: Henrik Böving module prelude -import Init.Data.Nat.Log2 +public import Init.Data.Nat.Log2 + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index ef65744546..d606b6d504 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -import Init.Core -import Init.Data.Int.Basic -import Init.Data.ToString.Basic +public import Init.Core +public import Init.Data.Int.Basic +public import Init.Data.ToString.Basic + +public section structure FloatSpec where float : Type diff --git a/src/Init/Data/Float32.lean b/src/Init/Data/Float32.lean index 08824d9736..d920da5fc8 100644 --- a/src/Init/Data/Float32.lean +++ b/src/Init/Data/Float32.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura module prelude -import Init.Core -import Init.Data.Int.Basic -import Init.Data.ToString.Basic -import Init.Data.Float +public import Init.Core +public import Init.Data.Int.Basic +public import Init.Data.ToString.Basic +public import Init.Data.Float + +public section -- Just show FloatSpec is inhabited. opaque float32Spec : FloatSpec := { diff --git a/src/Init/Data/FloatArray.lean b/src/Init/Data/FloatArray.lean index db5f314148..4dd9bd0808 100644 --- a/src/Init/Data/FloatArray.lean +++ b/src/Init/Data/FloatArray.lean @@ -6,4 +6,6 @@ Author: Leonardo de Moura module prelude -import Init.Data.FloatArray.Basic +public import Init.Data.FloatArray.Basic + +public section diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean index faf7174876..a0694e0e22 100644 --- a/src/Init/Data/FloatArray/Basic.lean +++ b/src/Init/Data/FloatArray/Basic.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import Init.Data.Array.Basic -import Init.Data.Float -import Init.Data.Option.Basic +public import Init.Data.Array.Basic +public import Init.Data.Float +public import Init.Data.Option.Basic + +public section universe u structure FloatArray where diff --git a/src/Init/Data/Format.lean b/src/Init/Data/Format.lean index a64639991c..6537fd89a6 100644 --- a/src/Init/Data/Format.lean +++ b/src/Init/Data/Format.lean @@ -6,7 +6,9 @@ Author: Leonardo de Moura module prelude -import Init.Data.Format.Basic -import Init.Data.Format.Macro -import Init.Data.Format.Instances -import Init.Data.Format.Syntax +public import Init.Data.Format.Basic +public import Init.Data.Format.Macro +public import Init.Data.Format.Instances +public import Init.Data.Format.Syntax + +public section diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index 0d6d657cc2..594434533d 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import Init.Control.State -import Init.Data.Int.Basic -import Init.Data.String.Basic +public import Init.Control.State +public import Init.Data.Int.Basic +public import Init.Data.String.Basic + +public section namespace Std diff --git a/src/Init/Data/Format/Instances.lean b/src/Init/Data/Format/Instances.lean index 1df47e08a6..a19c919b35 100644 --- a/src/Init/Data/Format/Instances.lean +++ b/src/Init/Data/Format/Instances.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import Init.Data.Format.Basic -import Init.Data.Array.Basic -import Init.Data.ToString.Basic +public import Init.Data.Format.Basic +public import Init.Data.Array.Basic +public import Init.Data.ToString.Basic + +public section open Std diff --git a/src/Init/Data/Format/Macro.lean b/src/Init/Data/Format/Macro.lean index 85e42a603e..c426669d13 100644 --- a/src/Init/Data/Format/Macro.lean +++ b/src/Init/Data/Format/Macro.lean @@ -6,8 +6,10 @@ Author: Leonardo de Moura module prelude -import Init.Data.Format.Basic -import Init.Data.ToString.Macro +public import Init.Data.Format.Basic +public import Init.Data.ToString.Macro + +public section namespace Std diff --git a/src/Init/Data/Format/Syntax.lean b/src/Init/Data/Format/Syntax.lean index 4f659ee038..3216c87063 100644 --- a/src/Init/Data/Format/Syntax.lean +++ b/src/Init/Data/Format/Syntax.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import Init.Data.Format.Macro -import Init.Data.Format.Instances -import Init.Meta +public import Init.Data.Format.Macro +public import Init.Data.Format.Instances +public import Init.Meta + +public section namespace Lean.Syntax diff --git a/src/Init/Data/Function.lean b/src/Init/Data/Function.lean index a081d01633..721b570ef5 100644 --- a/src/Init/Data/Function.lean +++ b/src/Init/Data/Function.lean @@ -7,7 +7,9 @@ Authors: Kim Morrison module prelude -import Init.Core +public import Init.Core + +public section namespace Function diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean index 1f8dbc57e9..15a7aa4ea8 100644 --- a/src/Init/Data/Hashable.lean +++ b/src/Init/Data/Hashable.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -import Init.Data.UInt.Basic -import Init.Data.String.Basic -import Init.Data.ByteArray.Basic +public import Init.Data.UInt.Basic +public import Init.Data.String.Basic +public import Init.Data.ByteArray.Basic + +public section universe u instance : Hashable Nat where diff --git a/src/Init/Data/Int.lean b/src/Init/Data/Int.lean index 82b7eff9b9..eb4d426b70 100644 --- a/src/Init/Data/Int.lean +++ b/src/Init/Data/Int.lean @@ -6,15 +6,17 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Int.Basic -import Init.Data.Int.Bitwise -import Init.Data.Int.Compare -import Init.Data.Int.DivMod -import Init.Data.Int.Gcd -import Init.Data.Int.Lemmas -import Init.Data.Int.LemmasAux -import Init.Data.Int.Order -import Init.Data.Int.Pow -import Init.Data.Int.Cooper -import Init.Data.Int.Linear -import Init.Data.Int.OfNat +public import Init.Data.Int.Basic +public import Init.Data.Int.Bitwise +public import Init.Data.Int.Compare +public import Init.Data.Int.DivMod +public import Init.Data.Int.Gcd +public import Init.Data.Int.Lemmas +public import Init.Data.Int.LemmasAux +public import Init.Data.Int.Order +public import Init.Data.Int.Pow +public import Init.Data.Int.Cooper +public import Init.Data.Int.Linear +public import Init.Data.Int.OfNat + +public section diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index ff236e11c0..e71b4adad0 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -8,8 +8,10 @@ The integers, with addition, multiplication, and subtraction. module prelude -import Init.Data.Cast -import Init.Data.Nat.Div.Basic +public import Init.Data.Cast +public import Init.Data.Nat.Div.Basic + +public section @[expose] section diff --git a/src/Init/Data/Int/Bitwise.lean b/src/Init/Data/Int/Bitwise.lean index 38623eb7cb..8b0506ceca 100644 --- a/src/Init/Data/Int/Bitwise.lean +++ b/src/Init/Data/Int/Bitwise.lean @@ -6,5 +6,7 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.Bitwise.Basic -import Init.Data.Int.Bitwise.Lemmas +public import Init.Data.Int.Bitwise.Basic +public import Init.Data.Int.Bitwise.Lemmas + +public section diff --git a/src/Init/Data/Int/Bitwise/Basic.lean b/src/Init/Data/Int/Bitwise/Basic.lean index 85f33bdc85..947a95f700 100644 --- a/src/Init/Data/Int/Bitwise/Basic.lean +++ b/src/Init/Data/Int/Bitwise/Basic.lean @@ -6,8 +6,10 @@ Authors: Mario Carneiro module prelude -import Init.Data.Int.Basic -import Init.Data.Nat.Bitwise.Basic +public import Init.Data.Int.Basic +public import Init.Data.Nat.Bitwise.Basic + +public section namespace Int diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index 6e0b81ee55..cc959d5a58 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -6,9 +6,11 @@ Authors: Siddharth Bhat, Jeremy Avigad module prelude -import Init.Data.Nat.Bitwise.Lemmas -import all Init.Data.Int.Bitwise.Basic -import Init.Data.Int.DivMod.Lemmas +public import Init.Data.Nat.Bitwise.Lemmas +public import all Init.Data.Int.Bitwise.Basic +public import Init.Data.Int.DivMod.Lemmas + +public section namespace Int diff --git a/src/Init/Data/Int/Compare.lean b/src/Init/Data/Int/Compare.lean index 7cab21715c..08710b9f70 100644 --- a/src/Init/Data/Int/Compare.lean +++ b/src/Init/Data/Int/Compare.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert module prelude -import all Init.Data.Ord -import Init.Data.Int.Order +public import all Init.Data.Ord +public import Init.Data.Int.Order + +public section /-! # Basic lemmas about comparing integers diff --git a/src/Init/Data/Int/Cooper.lean b/src/Init/Data/Int/Cooper.lean index 9e7e8e91e8..6c3def885f 100644 --- a/src/Init/Data/Int/Cooper.lean +++ b/src/Init/Data/Int/Cooper.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.DivMod.Lemmas -import Init.Data.Int.Gcd +public import Init.Data.Int.DivMod.Lemmas +public import Init.Data.Int.Gcd + +public section /-! ## Cooper resolution: small solutions to boundedness and divisibility constraints. diff --git a/src/Init/Data/Int/DivMod.lean b/src/Init/Data/Int/DivMod.lean index e095ae7579..cf883cf170 100644 --- a/src/Init/Data/Int/DivMod.lean +++ b/src/Init/Data/Int/DivMod.lean @@ -6,6 +6,8 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.DivMod.Basic -import Init.Data.Int.DivMod.Bootstrap -import Init.Data.Int.DivMod.Lemmas +public import Init.Data.Int.DivMod.Basic +public import Init.Data.Int.DivMod.Bootstrap +public import Init.Data.Int.DivMod.Lemmas + +public section diff --git a/src/Init/Data/Int/DivMod/Basic.lean b/src/Init/Data/Int/DivMod/Basic.lean index 8e89e76c4c..27658b8dd0 100644 --- a/src/Init/Data/Int/DivMod/Basic.lean +++ b/src/Init/Data/Int/DivMod/Basic.lean @@ -6,7 +6,9 @@ Authors: Jeremy Avigad, Mario Carneiro module prelude -import Init.Data.Int.Basic +public import Init.Data.Int.Basic + +public section @[expose] section diff --git a/src/Init/Data/Int/DivMod/Bootstrap.lean b/src/Init/Data/Int/DivMod/Bootstrap.lean index 2c91bce0b7..b481109bff 100644 --- a/src/Init/Data/Int/DivMod/Bootstrap.lean +++ b/src/Init/Data/Int/DivMod/Bootstrap.lean @@ -6,10 +6,12 @@ Authors: Jeremy Avigad, Mario Carneiro module prelude -import Init.Data.Int.DivMod.Basic -import Init.Data.Int.Order -import Init.Data.Nat.Dvd -import Init.RCases +public import Init.Data.Int.DivMod.Basic +public import Init.Data.Int.Order +public import Init.Data.Nat.Dvd +public import Init.RCases + +public section /-! # Lemmas about integer division needed to bootstrap `omega`. diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean index 0d1e880adb..69254cf445 100644 --- a/src/Init/Data/Int/DivMod/Lemmas.lean +++ b/src/Init/Data/Int/DivMod/Lemmas.lean @@ -6,13 +6,15 @@ Authors: Jeremy Avigad, Mario Carneiro, Kim Morrison, Markus Himmel module prelude -import Init.Data.Int.DivMod.Bootstrap -import Init.Data.Nat.Lemmas -import Init.Data.Nat.Div.Lemmas -import Init.Data.Int.Order -import Init.Data.Int.Lemmas -import Init.Data.Nat.Dvd -import Init.RCases +public import Init.Data.Int.DivMod.Bootstrap +public import Init.Data.Nat.Lemmas +public import Init.Data.Nat.Div.Lemmas +public import Init.Data.Int.Order +public import Init.Data.Int.Lemmas +public import Init.Data.Nat.Dvd +public import Init.RCases + +public section /-! # Further lemmas about integer division, now that `omega` is available. diff --git a/src/Init/Data/Int/Gcd.lean b/src/Init/Data/Int/Gcd.lean index 095df4011f..4cae3e0f4a 100644 --- a/src/Init/Data/Int/Gcd.lean +++ b/src/Init/Data/Int/Gcd.lean @@ -6,11 +6,13 @@ Authors: Mario Carneiro, Markus Himmel module prelude -import Init.Data.Int.Basic -import Init.Data.Nat.Gcd -import Init.Data.Nat.Lcm -import Init.Data.Int.DivMod.Lemmas -import Init.Data.Int.Pow +public import Init.Data.Int.Basic +public import Init.Data.Nat.Gcd +public import Init.Data.Nat.Lcm +public import Init.Data.Int.DivMod.Lemmas +public import Init.Data.Int.Pow + +public section /-! Definition and lemmas for gcd and lcm over Int diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean index 222c290f60..5fef6092d5 100644 --- a/src/Init/Data/Int/Lemmas.lean +++ b/src/Init/Data/Int/Lemmas.lean @@ -6,9 +6,11 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro module prelude -import Init.Conv -import Init.NotationExtra -import Init.PropLemmas +public import Init.Conv +public import Init.NotationExtra +public import Init.PropLemmas + +public section namespace Int diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 380e9710c0..683ff45a3e 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.Order -import Init.Data.Int.Pow -import Init.Data.Int.DivMod.Lemmas -import Init.Omega +public import Init.Data.Int.Order +public import Init.Data.Int.Pow +public import Init.Data.Int.DivMod.Lemmas +public import Init.Omega + +public section /-! diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index f1cf3bc2fe..b46ba794a6 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/src/Init/Data/Int/Linear.lean @@ -6,15 +6,17 @@ Authors: Leonardo de Moura module prelude -import Init.ByCases -import Init.Data.Prod -import Init.Data.Int.Lemmas -import Init.Data.Int.LemmasAux -import Init.Data.Int.DivMod.Bootstrap -import Init.Data.Int.Cooper -import all Init.Data.Int.Gcd -import Init.Data.RArray -import all Init.Data.AC +public import Init.ByCases +public import Init.Data.Prod +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.RArray +public import all Init.Data.AC + +public section namespace Int.Linear diff --git a/src/Init/Data/Int/OfNat.lean b/src/Init/Data/Int/OfNat.lean index 8976ac85f9..c389b0d673 100644 --- a/src/Init/Data/Int/OfNat.lean +++ b/src/Init/Data/Int/OfNat.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Int.Lemmas -import Init.Data.Int.DivMod -import Init.Data.Int.Linear -import Init.Data.RArray +public import Init.Data.Int.Lemmas +public import Init.Data.Int.DivMod +public import Init.Data.Int.Linear +public import Init.Data.RArray + +public section namespace Int.OfNat /-! diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean index 9e05ac2916..4035ca4711 100644 --- a/src/Init/Data/Int/Order.lean +++ b/src/Init/Data/Int/Order.lean @@ -6,8 +6,10 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro module prelude -import Init.Data.Int.Lemmas -import Init.ByCases +public import Init.Data.Int.Lemmas +public import Init.ByCases + +public section /-! # Results about the order properties of the integers, and the integers as an ordered ring. diff --git a/src/Init/Data/Int/Pow.lean b/src/Init/Data/Int/Pow.lean index e4ac2488f1..1c7a4f428e 100644 --- a/src/Init/Data/Int/Pow.lean +++ b/src/Init/Data/Int/Pow.lean @@ -6,8 +6,10 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro module prelude -import Init.Data.Int.Lemmas -import Init.Data.Nat.Lemmas +public import Init.Data.Int.Lemmas +public import Init.Data.Nat.Lemmas + +public section namespace Int diff --git a/src/Init/Data/Iterators.lean b/src/Init/Data/Iterators.lean index 1fde41993b..f6852070dd 100644 --- a/src/Init/Data/Iterators.lean +++ b/src/Init/Data/Iterators.lean @@ -6,13 +6,15 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic -import Init.Data.Iterators.PostconditionMonad -import Init.Data.Iterators.Consumers -import Init.Data.Iterators.Combinators -import Init.Data.Iterators.Lemmas -import Init.Data.Iterators.ToIterator -import Init.Data.Iterators.Internal +public import Init.Data.Iterators.Basic +public import Init.Data.Iterators.PostconditionMonad +public import Init.Data.Iterators.Consumers +public import Init.Data.Iterators.Combinators +public import Init.Data.Iterators.Lemmas +public import Init.Data.Iterators.ToIterator +public import Init.Data.Iterators.Internal + +public section /-! # Iterators diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean index eda5c08de7..b19a60d74e 100644 --- a/src/Init/Data/Iterators/Basic.lean +++ b/src/Init/Data/Iterators/Basic.lean @@ -6,11 +6,13 @@ Authors: Paul Reichert module prelude -import Init.Core -import Init.Classical -import Init.Ext -import Init.NotationExtra -import Init.TacticsExtra +public import Init.Core +public import Init.Classical +public import Init.Ext +public import Init.NotationExtra +public import Init.TacticsExtra + +public section /-! ### Definition of iterators diff --git a/src/Init/Data/Iterators/Combinators.lean b/src/Init/Data/Iterators/Combinators.lean index 8f56abe298..c48bdaa250 100644 --- a/src/Init/Data/Iterators/Combinators.lean +++ b/src/Init/Data/Iterators/Combinators.lean @@ -6,6 +6,8 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Combinators.Monadic -import Init.Data.Iterators.Combinators.FilterMap -import Init.Data.Iterators.Combinators.ULift +public import Init.Data.Iterators.Combinators.Monadic +public import Init.Data.Iterators.Combinators.FilterMap +public import Init.Data.Iterators.Combinators.ULift + +public section diff --git a/src/Init/Data/Iterators/Combinators/Attach.lean b/src/Init/Data/Iterators/Combinators/Attach.lean index 304e6c53c0..33961d65a6 100644 --- a/src/Init/Data/Iterators/Combinators/Attach.lean +++ b/src/Init/Data/Iterators/Combinators/Attach.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Combinators.Monadic.Attach -import Init.Data.Iterators.Combinators.FilterMap +public import Init.Data.Iterators.Combinators.Monadic.Attach +public import Init.Data.Iterators.Combinators.FilterMap + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Combinators/FilterMap.lean index c0e21c30a0..56c6b61272 100644 --- a/src/Init/Data/Iterators/Combinators/FilterMap.lean +++ b/src/Init/Data/Iterators/Combinators/FilterMap.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Combinators.Monadic.FilterMap +public import Init.Data.Iterators.Combinators.Monadic.FilterMap + +public section /-! diff --git a/src/Init/Data/Iterators/Combinators/Monadic.lean b/src/Init/Data/Iterators/Combinators/Monadic.lean index 34b0bc5b43..e02c2d097f 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic.lean @@ -6,5 +6,7 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Combinators.Monadic.FilterMap -import Init.Data.Iterators.Combinators.Monadic.ULift +public import Init.Data.Iterators.Combinators.Monadic.FilterMap +public import Init.Data.Iterators.Combinators.Monadic.ULift + +public section diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean index 88e431c4b8..8bcc710c8b 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic -import Init.Data.Iterators.Internal.Termination -import Init.Data.Iterators.Consumers.Collect -import Init.Data.Iterators.Consumers.Loop +public import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Internal.Termination +public import Init.Data.Iterators.Consumers.Collect +public import Init.Data.Iterators.Consumers.Loop + +public section namespace Std.Iterators.Types diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean index 5b19a49fcd..8cf529c226 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean @@ -6,11 +6,13 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic -import Init.Data.Iterators.Consumers.Collect -import Init.Data.Iterators.Consumers.Loop -import Init.Data.Iterators.PostconditionMonad -import Init.Data.Iterators.Internal.Termination +public import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Consumers.Collect +public import Init.Data.Iterators.Consumers.Loop +public import Init.Data.Iterators.PostconditionMonad +public import Init.Data.Iterators.Internal.Termination + +public section /-! diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean index 0e3149d2e5..97d9750ce0 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic -import Init.Data.Iterators.Internal.Termination -import Init.Data.Iterators.Consumers.Monadic +public import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Internal.Termination +public import Init.Data.Iterators.Consumers.Monadic + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Combinators/ULift.lean b/src/Init/Data/Iterators/Combinators/ULift.lean index ad9e8f7283..23ca5809ad 100644 --- a/src/Init/Data/Iterators/Combinators/ULift.lean +++ b/src/Init/Data/Iterators/Combinators/ULift.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Combinators.Monadic.ULift +public import Init.Data.Iterators.Combinators.Monadic.ULift + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Consumers.lean b/src/Init/Data/Iterators/Consumers.lean index e61fab7a94..e4c4aedc49 100644 --- a/src/Init/Data/Iterators/Consumers.lean +++ b/src/Init/Data/Iterators/Consumers.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Consumers.Monadic -import Init.Data.Iterators.Consumers.Access -import Init.Data.Iterators.Consumers.Collect -import Init.Data.Iterators.Consumers.Loop -import Init.Data.Iterators.Consumers.Partial +public import Init.Data.Iterators.Consumers.Monadic +public import Init.Data.Iterators.Consumers.Access +public import Init.Data.Iterators.Consumers.Collect +public import Init.Data.Iterators.Consumers.Loop +public import Init.Data.Iterators.Consumers.Partial + +public section diff --git a/src/Init/Data/Iterators/Consumers/Access.lean b/src/Init/Data/Iterators/Consumers/Access.lean index d99400341b..d845a787c6 100644 --- a/src/Init/Data/Iterators/Consumers/Access.lean +++ b/src/Init/Data/Iterators/Consumers/Access.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Data.Stream -import Init.Data.Iterators.Consumers.Partial -import Init.Data.Iterators.Consumers.Loop -import Init.Data.Iterators.Consumers.Monadic.Access +public import Init.Data.Stream +public import Init.Data.Iterators.Consumers.Partial +public import Init.Data.Iterators.Consumers.Loop +public import Init.Data.Iterators.Consumers.Monadic.Access + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Consumers/Collect.lean b/src/Init/Data/Iterators/Consumers/Collect.lean index fd848dfd55..a12b000a7b 100644 --- a/src/Init/Data/Iterators/Consumers/Collect.lean +++ b/src/Init/Data/Iterators/Consumers/Collect.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic -import Init.Data.Iterators.Consumers.Partial -import Init.Data.Iterators.Consumers.Monadic.Collect +public import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Consumers.Partial +public import Init.Data.Iterators.Consumers.Monadic.Collect + +public section /-! # Collectors diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean index ca0c0ccc34..c27a5e7db0 100644 --- a/src/Init/Data/Iterators/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Loop.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Consumers.Collect -import Init.Data.Iterators.Consumers.Monadic.Loop -import Init.Data.Iterators.Consumers.Partial +public import Init.Data.Iterators.Consumers.Collect +public import Init.Data.Iterators.Consumers.Monadic.Loop +public import Init.Data.Iterators.Consumers.Partial + +public section /-! # Loop consumers diff --git a/src/Init/Data/Iterators/Consumers/Monadic.lean b/src/Init/Data/Iterators/Consumers/Monadic.lean index 224348f971..c8bec732b5 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Consumers.Monadic.Access -import Init.Data.Iterators.Consumers.Monadic.Collect -import Init.Data.Iterators.Consumers.Monadic.Loop -import Init.Data.Iterators.Consumers.Monadic.Partial +public import Init.Data.Iterators.Consumers.Monadic.Access +public import Init.Data.Iterators.Consumers.Monadic.Collect +public import Init.Data.Iterators.Consumers.Monadic.Loop +public import Init.Data.Iterators.Consumers.Monadic.Partial + +public section diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean index 8aac369ed8..4eafb0c32a 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Basic + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean index e0e714943c..dae6c21774 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Consumers.Monadic.Partial -import Init.Data.Iterators.Internal.LawfulMonadLiftFunction +public import Init.Data.Iterators.Consumers.Monadic.Partial +public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction + +public section /-! # Collectors diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index 383c8decd0..b5a84bd42e 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import Init.RCases -import Init.Data.Iterators.Basic -import Init.Data.Iterators.Consumers.Monadic.Partial +public import Init.RCases +public import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Consumers.Monadic.Partial + +public section /-! # Loop-based consumers diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean b/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean index 5f87ab2cb5..6fb3e7930c 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Basic + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Consumers/Partial.lean b/src/Init/Data/Iterators/Consumers/Partial.lean index 2823d318b2..6a9f7f59d6 100644 --- a/src/Init/Data/Iterators/Consumers/Partial.lean +++ b/src/Init/Data/Iterators/Consumers/Partial.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Basic + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Internal.lean b/src/Init/Data/Iterators/Internal.lean index 2728123f13..8dfbaf3501 100644 --- a/src/Init/Data/Iterators/Internal.lean +++ b/src/Init/Data/Iterators/Internal.lean @@ -6,5 +6,7 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Internal.LawfulMonadLiftFunction -import Init.Data.Iterators.Internal.Termination +public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction +public import Init.Data.Iterators.Internal.Termination + +public section diff --git a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean index b011065a5c..e03702fe03 100644 --- a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean +++ b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Control.Basic -import Init.Control.Lawful.Basic -import Init.NotationExtra -import Init.Control.Lawful.MonadLift +public import Init.Control.Basic +public import Init.Control.Lawful.Basic +public import Init.NotationExtra +public import Init.Control.Lawful.MonadLift + +public section /-! # Typeclass for lawful monad lifting functions diff --git a/src/Init/Data/Iterators/Internal/Termination.lean b/src/Init/Data/Iterators/Internal/Termination.lean index 0229464884..324e0191bc 100644 --- a/src/Init/Data/Iterators/Internal/Termination.lean +++ b/src/Init/Data/Iterators/Internal/Termination.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Basic + +public section /-! This is an internal module used by iterator implementations. diff --git a/src/Init/Data/Iterators/Lemmas.lean b/src/Init/Data/Iterators/Lemmas.lean index 6a4e33f659..ad0af047a5 100644 --- a/src/Init/Data/Iterators/Lemmas.lean +++ b/src/Init/Data/Iterators/Lemmas.lean @@ -6,5 +6,7 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Consumers -import Init.Data.Iterators.Lemmas.Combinators +public import Init.Data.Iterators.Lemmas.Consumers +public import Init.Data.Iterators.Lemmas.Combinators + +public section diff --git a/src/Init/Data/Iterators/Lemmas/Basic.lean b/src/Init/Data/Iterators/Lemmas/Basic.lean index dc8733e83d..690b1bf74b 100644 --- a/src/Init/Data/Iterators/Lemmas/Basic.lean +++ b/src/Init/Data/Iterators/Lemmas/Basic.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Basic + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Combinators.lean b/src/Init/Data/Iterators/Lemmas/Combinators.lean index 059783aa1c..e57ea267ac 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Combinators.Attach -import Init.Data.Iterators.Lemmas.Combinators.Monadic -import Init.Data.Iterators.Lemmas.Combinators.FilterMap -import Init.Data.Iterators.Lemmas.Combinators.ULift +public import Init.Data.Iterators.Lemmas.Combinators.Attach +public import Init.Data.Iterators.Lemmas.Combinators.Monadic +public import Init.Data.Iterators.Lemmas.Combinators.FilterMap +public import Init.Data.Iterators.Lemmas.Combinators.ULift + +public section diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean index 999b4c9908..c586485a0d 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import all Init.Data.Iterators.Combinators.Attach -import all Init.Data.Iterators.Combinators.Monadic.Attach -import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach -import Init.Data.Iterators.Lemmas.Consumers.Collect +public import all Init.Data.Iterators.Combinators.Attach +public 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 section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean index d4305c227d..0d7c4d2e7b 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Consumers -import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap -import Init.Data.Iterators.Combinators.FilterMap +public import Init.Data.Iterators.Lemmas.Consumers +public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap +public import Init.Data.Iterators.Combinators.FilterMap + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean index 6a2aa3ee8f..d707eec87a 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean @@ -6,6 +6,8 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach -import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap -import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift +public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach +public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap +public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift + +public section diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean index 5c3aaa5dbf..11b7335b13 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import all Init.Data.Iterators.Combinators.Monadic.Attach -import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect +public import all Init.Data.Iterators.Combinators.Monadic.Attach +public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean index 12c8e1ab55..8d18a55228 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Internal.LawfulMonadLiftFunction -import Init.Data.Iterators.Combinators.Monadic.FilterMap -import Init.Data.Iterators.Lemmas.Consumers.Monadic -import all Init.Data.Iterators.Consumers.Monadic.Collect +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 section namespace Std.Iterators open Std.Internal diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean index 4232473a73..c4f3f02902 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import all Init.Data.Iterators.Combinators.Monadic.ULift -import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect +public import all Init.Data.Iterators.Combinators.Monadic.ULift +public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean index ca6b7e6b15..5589910906 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import all Init.Data.Iterators.Combinators.ULift -import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift -import Init.Data.Iterators.Lemmas.Consumers.Collect +public import all Init.Data.Iterators.Combinators.ULift +public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift +public import Init.Data.Iterators.Lemmas.Consumers.Collect + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Consumers.lean b/src/Init/Data/Iterators/Lemmas/Consumers.lean index a363ee747f..b6cae0c957 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers.lean @@ -6,6 +6,8 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Consumers.Monadic -import Init.Data.Iterators.Lemmas.Consumers.Collect -import Init.Data.Iterators.Lemmas.Consumers.Loop +public import Init.Data.Iterators.Lemmas.Consumers.Monadic +public import Init.Data.Iterators.Lemmas.Consumers.Collect +public import Init.Data.Iterators.Lemmas.Consumers.Loop + +public section diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean index c7d345433b..f1457a8735 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Basic -import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect -import all Init.Data.Iterators.Consumers.Access -import all Init.Data.Iterators.Consumers.Collect +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 section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index b3c4d101f3..ceb63c0b80 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Consumers.Collect -import all Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop -import all Init.Data.Iterators.Consumers.Loop -import all Init.Data.Iterators.Consumers.Monadic.Collect +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 section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean index bcbc5fd29f..5e60a3b4fb 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean @@ -6,5 +6,7 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect -import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop +public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect +public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop + +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 2a36e8e26a..92fe39179f 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import Init.Data.Array.Lemmas -import Init.Data.Iterators.Lemmas.Monadic.Basic -import all Init.Data.Iterators.Consumers.Monadic.Collect +public import Init.Data.Array.Lemmas +public import Init.Data.Iterators.Lemmas.Monadic.Basic +public import all Init.Data.Iterators.Consumers.Monadic.Collect + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean index a34202c93f..0182a979bc 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect -import all Init.Data.Iterators.Consumers.Monadic.Loop +public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect +public import all Init.Data.Iterators.Consumers.Monadic.Loop + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean b/src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean index 3753c26f9d..d02bf9f16c 100644 --- a/src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean +++ b/src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Basic +public import Init.Data.Iterators.Basic + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/PostconditionMonad.lean b/src/Init/Data/Iterators/PostconditionMonad.lean index 923d2c6d1c..a59dc253f1 100644 --- a/src/Init/Data/Iterators/PostconditionMonad.lean +++ b/src/Init/Data/Iterators/PostconditionMonad.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import Init.Control.Lawful.Basic -import Init.Data.Subtype -import Init.PropLemmas +public import Init.Control.Lawful.Basic +public import Init.Data.Subtype +public import Init.PropLemmas + +public section namespace Std.Iterators diff --git a/src/Init/Data/Iterators/ToIterator.lean b/src/Init/Data/Iterators/ToIterator.lean index 51bc258e3a..eaa1d04455 100644 --- a/src/Init/Data/Iterators/ToIterator.lean +++ b/src/Init/Data/Iterators/ToIterator.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Consumers +public import Init.Data.Iterators.Consumers + +public section /-! This module provides the typeclass `ToIterator`, which is implemented by types that can be diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean index 81be021a26..59bbe26951 100644 --- a/src/Init/Data/List.lean +++ b/src/Init/Data/List.lean @@ -6,28 +6,30 @@ Authors: Leonardo de Moura module prelude -import Init.Data.List.Attach -import Init.Data.List.Basic -import Init.Data.List.BasicAux -import Init.Data.List.Control -import Init.Data.List.Count -import Init.Data.List.Erase -import Init.Data.List.Find -import Init.Data.List.Impl -import Init.Data.List.Lemmas -import Init.Data.List.MinMax -import Init.Data.List.Monadic -import Init.Data.List.Nat -import Init.Data.List.Notation -import Init.Data.List.Pairwise -import Init.Data.List.Sublist -import Init.Data.List.TakeDrop -import Init.Data.List.Zip -import Init.Data.List.Perm -import Init.Data.List.Sort -import Init.Data.List.ToArray -import Init.Data.List.ToArrayImpl -import Init.Data.List.MapIdx -import Init.Data.List.OfFn -import Init.Data.List.FinRange -import Init.Data.List.Lex +public import Init.Data.List.Attach +public import Init.Data.List.Basic +public import Init.Data.List.BasicAux +public import Init.Data.List.Control +public import Init.Data.List.Count +public import Init.Data.List.Erase +public import Init.Data.List.Find +public import Init.Data.List.Impl +public import Init.Data.List.Lemmas +public import Init.Data.List.MinMax +public import Init.Data.List.Monadic +public import Init.Data.List.Nat +public import Init.Data.List.Notation +public import Init.Data.List.Pairwise +public import Init.Data.List.Sublist +public import Init.Data.List.TakeDrop +public import Init.Data.List.Zip +public import Init.Data.List.Perm +public import Init.Data.List.Sort +public import Init.Data.List.ToArray +public import Init.Data.List.ToArrayImpl +public import Init.Data.List.MapIdx +public import Init.Data.List.OfFn +public import Init.Data.List.FinRange +public import Init.Data.List.Lex + +public section diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 0cb45de9fb..3d3b6f30a6 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -6,10 +6,12 @@ Authors: Mario Carneiro module prelude -import all Init.Data.List.Lemmas -- for dsimping with `getElem?_cons_succ` -import Init.Data.List.Count -import Init.Data.Subtype -import Init.BinderNameHint +public import all Init.Data.List.Lemmas -- for dsimping with `getElem?_cons_succ` +public import Init.Data.List.Count +public import Init.Data.Subtype +public import Init.BinderNameHint + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 87dd2a5c25..aad728f5a8 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -6,10 +6,12 @@ Author: Leonardo de Moura module prelude -import Init.SimpLemmas -import Init.Data.Nat.Basic -import Init.Data.List.Notation -import Init.Data.Nat.Div.Basic +public import Init.SimpLemmas +public import Init.Data.Nat.Basic +public import Init.Data.List.Notation +public import Init.Data.Nat.Div.Basic + +public section @[expose] section diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index f6f7ca13ce..7c91a758ce 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -6,7 +6,9 @@ Author: Leonardo de Moura module prelude -import Init.Data.Nat.Linear +public import Init.Data.Nat.Linear + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 04af7c236a..71caec2596 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import Init.Control.Basic -import Init.Control.Id -import Init.Control.Lawful +public import Init.Control.Basic +public import Init.Control.Id +public import Init.Control.Lawful + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index 1b3c72ab4d..2727111c10 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -6,7 +6,9 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Sublist +public import Init.Data.List.Sublist + +public section /-! # Lemmas about `List.countP` and `List.count`. diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean index e241c2b333..f55fc86144 100644 --- a/src/Init/Data/List/Erase.lean +++ b/src/Init/Data/List/Erase.lean @@ -7,8 +7,10 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Pairwise -import Init.Data.List.Find +public import Init.Data.List.Pairwise +public import Init.Data.List.Find + +public section /-! # Lemmas about `List.eraseP`, `List.erase`, and `List.eraseIdx`. diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean index 560bb6ddc2..72f1f86f3c 100644 --- a/src/Init/Data/List/FinRange.lean +++ b/src/Init/Data/List/FinRange.lean @@ -6,8 +6,10 @@ Authors: François G. Dorais module prelude -import all Init.Data.List.OfFn -import Init.Data.List.Monadic +public import all Init.Data.List.OfFn +public import Init.Data.List.Monadic + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 6378814dc8..67b676a160 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -7,12 +7,14 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Lemmas -import Init.Data.List.Sublist -import Init.Data.List.Range -import Init.Data.List.Impl -import all Init.Data.List.Attach -import Init.Data.Fin.Lemmas +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.Fin.Lemmas + +public section /-! Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `List.idxOf`, diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index f3258bc6b7..f3724757f8 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Array.Bootstrap +public import Init.Data.Array.Bootstrap + +public section /-! ## Tail recursive implementations for `List` definitions. diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index a1e8566100..1b3e042097 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -7,12 +7,14 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.Bool -import Init.Data.Option.Lemmas -import all Init.Data.List.BasicAux -import all Init.Data.List.Control -import Init.Control.Lawful.Basic -import Init.BinderPredicates +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.Control.Lawful.Basic +public import Init.BinderPredicates + +public section /-! # Theorems about `List` operations. diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean index e27b034560..dafb8a5c31 100644 --- a/src/Init/Data/List/Lex.lean +++ b/src/Init/Data/List/Lex.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Lemmas -import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Lemmas +public import Init.Data.List.Nat.TakeDrop + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index 52b79bac05..b672312596 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -7,11 +7,13 @@ Authors: Kim Morrison, Mario Carneiro module prelude -import Init.Data.Array.Lemmas -import Init.Data.List.Nat.Range -import Init.Data.List.OfFn -import Init.Data.Fin.Lemmas -import Init.Data.Option.Attach +public import Init.Data.Array.Lemmas +public import Init.Data.List.Nat.Range +public import Init.Data.List.OfFn +public import Init.Data.Fin.Lemmas +public import Init.Data.Option.Attach + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/MinMax.lean b/src/Init/Data/List/MinMax.lean index 4c18f47c63..47aa50a8e9 100644 --- a/src/Init/Data/List/MinMax.lean +++ b/src/Init/Data/List/MinMax.lean @@ -6,8 +6,10 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Lemmas -import Init.Data.List.Pairwise +public import Init.Data.List.Lemmas +public import Init.Data.List.Pairwise + +public section /-! # Lemmas about `List.min?` and `List.max?. diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean index ad2e734807..e3542bdf4b 100644 --- a/src/Init/Data/List/Monadic.lean +++ b/src/Init/Data/List/Monadic.lean @@ -6,11 +6,13 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.TakeDrop -import Init.Data.List.Attach -import Init.Data.List.OfFn -import Init.Data.Array.Bootstrap -import all Init.Data.List.Control +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 section /-! # Lemmas about `List.mapM` and `List.forM`. diff --git a/src/Init/Data/List/Nat.lean b/src/Init/Data/List/Nat.lean index 4806c9804a..fcaad2266c 100644 --- a/src/Init/Data/List/Nat.lean +++ b/src/Init/Data/List/Nat.lean @@ -6,15 +6,17 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Nat.Basic -import Init.Data.List.Nat.Pairwise -import Init.Data.List.Nat.Range -import Init.Data.List.Nat.Sublist -import Init.Data.List.Nat.TakeDrop -import Init.Data.List.Nat.Count -import Init.Data.List.Nat.Erase -import Init.Data.List.Nat.Find -import Init.Data.List.Nat.BEq -import Init.Data.List.Nat.Modify -import Init.Data.List.Nat.InsertIdx -import Init.Data.List.Nat.Perm +public import Init.Data.List.Nat.Basic +public import Init.Data.List.Nat.Pairwise +public import Init.Data.List.Nat.Range +public import Init.Data.List.Nat.Sublist +public import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Nat.Count +public import Init.Data.List.Nat.Erase +public import Init.Data.List.Nat.Find +public import Init.Data.List.Nat.BEq +public import Init.Data.List.Nat.Modify +public import Init.Data.List.Nat.InsertIdx +public import Init.Data.List.Nat.Perm + +public section diff --git a/src/Init/Data/List/Nat/BEq.lean b/src/Init/Data/List/Nat/BEq.lean index fbb503df8c..d4b0031a44 100644 --- a/src/Init/Data/List/Nat/BEq.lean +++ b/src/Init/Data/List/Nat/BEq.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Nat.Lemmas -import Init.Data.List.Basic +public import Init.Data.Nat.Lemmas +public import Init.Data.List.Basic + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index 8166ce106c..18cb224cea 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -6,10 +6,12 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Count -import Init.Data.List.Find -import Init.Data.List.MinMax -import Init.Data.Nat.Lemmas +public import Init.Data.List.Count +public import Init.Data.List.Find +public import Init.Data.List.MinMax +public import Init.Data.Nat.Lemmas + +public section /-! # Miscellaneous `List` lemmas, that require more `Nat` lemmas than are available in `Init.Data.List.Lemmas`. diff --git a/src/Init/Data/List/Nat/Count.lean b/src/Init/Data/List/Nat/Count.lean index d98d56e48f..5d212ac322 100644 --- a/src/Init/Data/List/Nat/Count.lean +++ b/src/Init/Data/List/Nat/Count.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Count -import Init.Data.Nat.Lemmas +public import Init.Data.List.Count +public import Init.Data.Nat.Lemmas + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Nat/Erase.lean b/src/Init/Data/List/Nat/Erase.lean index 625fcf102d..ff3f8fb9fe 100644 --- a/src/Init/Data/List/Nat/Erase.lean +++ b/src/Init/Data/List/Nat/Erase.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Nat.TakeDrop -import Init.Data.List.Erase +public import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Erase + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Nat/Find.lean b/src/Init/Data/List/Nat/Find.lean index e63728baf0..933118068c 100644 --- a/src/Init/Data/List/Nat/Find.lean +++ b/src/Init/Data/List/Nat/Find.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Nat.Range -import Init.Data.List.Find +public import Init.Data.List.Nat.Range +public import Init.Data.List.Find + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Nat/InsertIdx.lean b/src/Init/Data/List/Nat/InsertIdx.lean index db5047e309..18b80e380c 100644 --- a/src/Init/Data/List/Nat/InsertIdx.lean +++ b/src/Init/Data/List/Nat/InsertIdx.lean @@ -6,7 +6,9 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Nat.Modify +public import Init.Data.List.Nat.Modify + +public section /-! # insertIdx diff --git a/src/Init/Data/List/Nat/Modify.lean b/src/Init/Data/List/Nat/Modify.lean index 56f7622015..a2b510baa2 100644 --- a/src/Init/Data/List/Nat/Modify.lean +++ b/src/Init/Data/List/Nat/Modify.lean @@ -7,8 +7,10 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Nat.TakeDrop -import Init.Data.List.Nat.Erase +public import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Nat.Erase + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Nat/Pairwise.lean b/src/Init/Data/List/Nat/Pairwise.lean index 14cdff9324..a8fd296cf6 100644 --- a/src/Init/Data/List/Nat/Pairwise.lean +++ b/src/Init/Data/List/Nat/Pairwise.lean @@ -6,9 +6,11 @@ Authors: Mario Carneiro, James Gallicchio module prelude -import Init.Data.Fin.Lemmas -import Init.Data.List.Nat.TakeDrop -import Init.Data.List.Pairwise +public import Init.Data.Fin.Lemmas +public import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Pairwise + +public section /-! # Lemmas about `List.Pairwise` diff --git a/src/Init/Data/List/Nat/Perm.lean b/src/Init/Data/List/Nat/Perm.lean index 61d106f62a..395f0f40be 100644 --- a/src/Init/Data/List/Nat/Perm.lean +++ b/src/Init/Data/List/Nat/Perm.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Nat.TakeDrop -import Init.Data.List.Perm +public import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Perm + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean index 8791f5efed..6a5ca02d72 100644 --- a/src/Init/Data/List/Nat/Range.lean +++ b/src/Init/Data/List/Nat/Range.lean @@ -6,11 +6,13 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Nat.TakeDrop -import Init.Data.List.Range -import Init.Data.List.Pairwise -import Init.Data.List.Find -import Init.Data.List.Erase +public import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Range +public import Init.Data.List.Pairwise +public import Init.Data.List.Find +public import Init.Data.List.Erase + +public section /-! # Lemmas about `List.range` and `List.enum` diff --git a/src/Init/Data/List/Nat/Sublist.lean b/src/Init/Data/List/Nat/Sublist.lean index 2b9a006d81..816987d11e 100644 --- a/src/Init/Data/List/Nat/Sublist.lean +++ b/src/Init/Data/List/Nat/Sublist.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Sublist -import Init.Data.List.Nat.Basic -import Init.Data.List.Nat.TakeDrop -import Init.Data.Nat.Lemmas +public import Init.Data.List.Sublist +public import Init.Data.List.Nat.Basic +public import Init.Data.List.Nat.TakeDrop +public import Init.Data.Nat.Lemmas + +public section /-! # Further lemmas about `List.IsSuffix` / `List.IsPrefix` / `List.IsInfix`. diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index 33d6349fa6..c6537b8fc9 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -6,10 +6,12 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Zip -import Init.Data.List.Sublist -import Init.Data.List.Find -import Init.Data.Nat.Lemmas +public import Init.Data.List.Zip +public import Init.Data.List.Sublist +public import Init.Data.List.Find +public import Init.Data.Nat.Lemmas + +public section /-! # Further lemmas about `List.take`, `List.drop`, `List.zip` and `List.zipWith`. diff --git a/src/Init/Data/List/Notation.lean b/src/Init/Data/List/Notation.lean index fa17b43a87..4b61b8c403 100644 --- a/src/Init/Data/List/Notation.lean +++ b/src/Init/Data/List/Notation.lean @@ -6,7 +6,9 @@ Author: Leonardo de Moura module prelude -meta import Init.Data.Nat.Div.Basic +public meta import Init.Data.Nat.Div.Basic + +public section /-! # Notation for `List` literals. diff --git a/src/Init/Data/List/OfFn.lean b/src/Init/Data/List/OfFn.lean index ae581aca6a..cc8b1b5768 100644 --- a/src/Init/Data/List/OfFn.lean +++ b/src/Init/Data/List/OfFn.lean @@ -6,8 +6,10 @@ Authors: Mario Carneiro, Kim Morrison module prelude -import Init.Data.List.Basic -import Init.Data.Fin.Fold +public import Init.Data.List.Basic +public import Init.Data.Fin.Fold + +public section /-! # Theorems about `List.ofFn` diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean index 5bb79f41d7..2d2dd1eb95 100644 --- a/src/Init/Data/List/Pairwise.lean +++ b/src/Init/Data/List/Pairwise.lean @@ -6,8 +6,10 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Sublist -import Init.Data.List.Attach +public import Init.Data.List.Sublist +public import Init.Data.List.Attach + +public section /-! # Lemmas about `List.Pairwise` and `List.Nodup`. diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean index bc86e88793..23eb6848a0 100644 --- a/src/Init/Data/List/Perm.lean +++ b/src/Init/Data/List/Perm.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro module prelude -import Init.Data.List.Pairwise -import Init.Data.List.Erase -import Init.Data.List.Find -import all Init.Data.List.Attach +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 section /-! # List Permutations diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean index cf66d5ebc1..9b30b3b568 100644 --- a/src/Init/Data/List/Range.lean +++ b/src/Init/Data/List/Range.lean @@ -6,8 +6,10 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.Pairwise -import Init.Data.List.Zip +public import Init.Data.List.Pairwise +public import Init.Data.List.Zip + +public section /-! # Lemmas about `List.range` and `List.zipIdx` diff --git a/src/Init/Data/List/Sort.lean b/src/Init/Data/List/Sort.lean index 887f40ac41..292dd5d2a8 100644 --- a/src/Init/Data/List/Sort.lean +++ b/src/Init/Data/List/Sort.lean @@ -6,6 +6,8 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Sort.Basic -import Init.Data.List.Sort.Impl -import Init.Data.List.Sort.Lemmas +public import Init.Data.List.Sort.Basic +public import Init.Data.List.Sort.Impl +public import Init.Data.List.Sort.Lemmas + +public section diff --git a/src/Init/Data/List/Sort/Basic.lean b/src/Init/Data/List/Sort/Basic.lean index 50616a5ff4..1e49ee506f 100644 --- a/src/Init/Data/List/Sort/Basic.lean +++ b/src/Init/Data/List/Sort/Basic.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Impl -import Init.Data.List.Nat.TakeDrop +public import Init.Data.List.Impl +public import Init.Data.List.Nat.TakeDrop + +public section /-! # Definition of `merge` and `mergeSort`. diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean index c38f81a39c..c3a0538838 100644 --- a/src/Init/Data/List/Sort/Impl.lean +++ b/src/Init/Data/List/Sort/Impl.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import all Init.Data.List.Sort.Basic -import Init.Data.List.Sort.Lemmas +public import all Init.Data.List.Sort.Basic +public import Init.Data.List.Sort.Lemmas + +public section /-! # Replacing `merge` and `mergeSort` at runtime with tail-recursive and faster versions. diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index 229b191556..c6fc85a9ec 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison, Eric Wieser, François G. Dorais module prelude -import Init.Data.List.Perm -import all Init.Data.List.Sort.Basic -import Init.Data.List.Nat.Range -import Init.Data.Bool +public import Init.Data.List.Perm +public import all Init.Data.List.Sort.Basic +public import Init.Data.List.Nat.Range +public import Init.Data.Bool + +public section /-! # Basic properties of `mergeSort`. diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 3c27e217b8..55a4e27a64 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -7,7 +7,9 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.TakeDrop +public import Init.Data.List.TakeDrop + +public section /-! # Lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`. diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index d0d24daf83..af5e13f7c8 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -6,8 +6,10 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import all Init.Data.List.Basic -import Init.Data.List.Lemmas +public import all Init.Data.List.Basic +public import Init.Data.List.Lemmas + +public section /-! # Lemmas about `List.take` and `List.drop`. diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 3efadddcd3..59fc0ada6f 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -6,14 +6,16 @@ Authors: Mario Carneiro module prelude -import all Init.Data.List.Control -import Init.Data.List.Impl -import Init.Data.List.Nat.Erase -import Init.Data.List.Monadic -import Init.Data.List.Nat.InsertIdx -import Init.Data.Array.Lex.Basic -import all Init.Data.Array.Basic -import all Init.Data.Array.Set +public 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 section /-! ### Lemmas about `List.toArray`. diff --git a/src/Init/Data/List/ToArrayImpl.lean b/src/Init/Data/List/ToArrayImpl.lean index 1611ad9fc5..3cde4c8036 100644 --- a/src/Init/Data/List/ToArrayImpl.lean +++ b/src/Init/Data/List/ToArrayImpl.lean @@ -6,7 +6,9 @@ Authors: Henrik Böving module prelude -import Init.Data.List.Basic +public import Init.Data.List.Basic + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index fbbdb84ece..9ed4871012 100644 --- a/src/Init/Data/List/Zip.lean +++ b/src/Init/Data/List/Zip.lean @@ -6,8 +6,10 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module prelude -import Init.Data.List.TakeDrop -import Init.Data.Function +public import Init.Data.List.TakeDrop +public import Init.Data.Function + +public section /-! # Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`. diff --git a/src/Init/Data/Nat.lean b/src/Init/Data/Nat.lean index 73d3e73792..03291df1c5 100644 --- a/src/Init/Data/Nat.lean +++ b/src/Init/Data/Nat.lean @@ -6,20 +6,22 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Nat.Basic -import Init.Data.Nat.Div -import Init.Data.Nat.Dvd -import Init.Data.Nat.Gcd -import Init.Data.Nat.MinMax -import Init.Data.Nat.Bitwise -import Init.Data.Nat.Control -import Init.Data.Nat.Log2 -import Init.Data.Nat.Power2 -import Init.Data.Nat.Linear -import Init.Data.Nat.SOM -import Init.Data.Nat.Lemmas -import Init.Data.Nat.Mod -import Init.Data.Nat.Lcm -import Init.Data.Nat.Compare -import Init.Data.Nat.Simproc -import Init.Data.Nat.Fold +public import Init.Data.Nat.Basic +public import Init.Data.Nat.Div +public import Init.Data.Nat.Dvd +public import Init.Data.Nat.Gcd +public import Init.Data.Nat.MinMax +public import Init.Data.Nat.Bitwise +public import Init.Data.Nat.Control +public import Init.Data.Nat.Log2 +public import Init.Data.Nat.Power2 +public import Init.Data.Nat.Linear +public import Init.Data.Nat.SOM +public import Init.Data.Nat.Lemmas +public import Init.Data.Nat.Mod +public import Init.Data.Nat.Lcm +public import Init.Data.Nat.Compare +public import Init.Data.Nat.Simproc +public import Init.Data.Nat.Fold + +public section diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index f3a0c82772..1313940efd 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -6,9 +6,11 @@ Authors: Floris van Doorn, Leonardo de Moura module prelude -import Init.SimpLemmas -import Init.Data.NeZero -import Init.Grind.Tactics +public import Init.SimpLemmas +public import Init.Data.NeZero +public import Init.Grind.Tactics + +public section set_option linter.missingDocs true -- keep it documented universe u diff --git a/src/Init/Data/Nat/Bitwise.lean b/src/Init/Data/Nat/Bitwise.lean index 1988c1d6a3..a25b26edc8 100644 --- a/src/Init/Data/Nat/Bitwise.lean +++ b/src/Init/Data/Nat/Bitwise.lean @@ -6,5 +6,7 @@ Authors: Kim Morrison module prelude -import Init.Data.Nat.Bitwise.Basic -import Init.Data.Nat.Bitwise.Lemmas +public import Init.Data.Nat.Bitwise.Basic +public import Init.Data.Nat.Bitwise.Lemmas + +public section diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index 9cce6bf936..b1d374de80 100644 --- a/src/Init/Data/Nat/Bitwise/Basic.lean +++ b/src/Init/Data/Nat/Bitwise/Basic.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Nat.Basic -import Init.Data.Nat.Div.Basic -import Init.Coe +public import Init.Data.Nat.Basic +public import Init.Data.Nat.Div.Basic +public import Init.Coe + +public section namespace Nat diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index db32ab4981..cd5cbe3d93 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -7,12 +7,14 @@ Authors: Joe Hendrix module prelude -import Init.Data.Bool -import Init.Data.Int.Pow -import all Init.Data.Nat.Bitwise.Basic -import Init.Data.Nat.Lemmas -import Init.Data.Nat.Simproc -import Init.TacticsExtra +public import Init.Data.Bool +public import Init.Data.Int.Pow +public import all Init.Data.Nat.Bitwise.Basic +public import Init.Data.Nat.Lemmas +public import Init.Data.Nat.Simproc +public import Init.TacticsExtra + +public section /- This module defines properties of the bitwise operations on Natural numbers. diff --git a/src/Init/Data/Nat/Compare.lean b/src/Init/Data/Nat/Compare.lean index c8140b54e5..5a5e608783 100644 --- a/src/Init/Data/Nat/Compare.lean +++ b/src/Init/Data/Nat/Compare.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro module prelude -import all Init.Data.Ord +public import all Init.Data.Ord + +public section /-! # Basic lemmas about comparing natural numbers diff --git a/src/Init/Data/Nat/Control.lean b/src/Init/Data/Nat/Control.lean index ad482c21e4..47fc5861ff 100644 --- a/src/Init/Data/Nat/Control.lean +++ b/src/Init/Data/Nat/Control.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import Init.Control.Basic -import Init.Data.Nat.Basic -import Init.Omega +public import Init.Control.Basic +public import Init.Data.Nat.Basic +public import Init.Omega + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index 6673422d9f..d041f146a9 100644 --- a/src/Init/Data/Nat/Div.lean +++ b/src/Init/Data/Nat/Div.lean @@ -6,5 +6,7 @@ Authors: Kim Morrison module prelude -import Init.Data.Nat.Div.Basic -import Init.Data.Nat.Div.Lemmas +public import Init.Data.Nat.Div.Basic +public import Init.Data.Nat.Div.Lemmas + +public section diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean index 7211baa799..fbcd12c071 100644 --- a/src/Init/Data/Nat/Div/Basic.lean +++ b/src/Init/Data/Nat/Div/Basic.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura module prelude -import Init.WF -import Init.WFTactics -import Init.Data.Nat.Basic -meta import Init.MetaTypes +public import Init.WF +public import Init.WFTactics +public import Init.Data.Nat.Basic +public meta import Init.MetaTypes + +public section @[expose] section diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean index 98e22bc025..4b0bcc1d50 100644 --- a/src/Init/Data/Nat/Div/Lemmas.lean +++ b/src/Init/Data/Nat/Div/Lemmas.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Omega -import Init.Data.Nat.Lemmas -import Init.Data.Nat.Simproc +public import Init.Omega +public import Init.Data.Nat.Lemmas +public import Init.Data.Nat.Simproc + +public section /-! # Further lemmas about `Nat.div` and `Nat.mod`, with the convenience of having `omega` available. diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean index 36da6a440e..87a7ab0498 100644 --- a/src/Init/Data/Nat/Dvd.lean +++ b/src/Init/Data/Nat/Dvd.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro module prelude -import Init.Data.Nat.Div.Basic -import Init.Meta +public import Init.Data.Nat.Div.Basic +public import Init.Meta + +public section namespace Nat diff --git a/src/Init/Data/Nat/Fold.lean b/src/Init/Data/Nat/Fold.lean index c3df94e5be..563d30a069 100644 --- a/src/Init/Data/Nat/Fold.lean +++ b/src/Init/Data/Nat/Fold.lean @@ -6,8 +6,10 @@ Authors: Floris van Doorn, Leonardo de Moura, Kim Morrison module prelude -import Init.Omega -import Init.Data.List.FinRange +public import Init.Omega +public import Init.Data.List.FinRange + +public section set_option linter.missingDocs true -- keep it documented universe u diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean index 808a258968..67e57c50cb 100644 --- a/src/Init/Data/Nat/Gcd.lean +++ b/src/Init/Data/Nat/Gcd.lean @@ -6,9 +6,11 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Markus Himmel module prelude -import Init.Data.Nat.Dvd -import Init.NotationExtra -import Init.RCases +public import Init.Data.Nat.Dvd +public import Init.NotationExtra +public import Init.RCases + +public section namespace Nat diff --git a/src/Init/Data/Nat/Lcm.lean b/src/Init/Data/Nat/Lcm.lean index fc03680770..dccbd36ffa 100644 --- a/src/Init/Data/Nat/Lcm.lean +++ b/src/Init/Data/Nat/Lcm.lean @@ -6,8 +6,10 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Markus Himmel module prelude -import Init.Data.Nat.Gcd -import Init.Data.Nat.Lemmas +public import Init.Data.Nat.Gcd +public import Init.Data.Nat.Lemmas + +public section /-! # Lemmas about `Nat.lcm` diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 0ec01cc651..111b30055a 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -6,11 +6,13 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Floris van Doorn module prelude -import all Init.Data.Nat.Bitwise.Basic -import Init.Data.Nat.MinMax -import all Init.Data.Nat.Log2 -import Init.Data.Nat.Power2 -import Init.Data.Nat.Mod +public 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.Power2 +public import Init.Data.Nat.Mod + +public section /-! # Basic theorems about natural numbers diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean index 55e0c96689..ec09089674 100644 --- a/src/Init/Data/Nat/Linear.lean +++ b/src/Init/Data/Nat/Linear.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -import Init.ByCases -import Init.Data.Prod -import Init.Data.RArray +public import Init.ByCases +public import Init.Data.Prod +public import Init.Data.RArray + +public section @[expose] section diff --git a/src/Init/Data/Nat/Log2.lean b/src/Init/Data/Nat/Log2.lean index 5497e7d99c..da2f60c147 100644 --- a/src/Init/Data/Nat/Log2.lean +++ b/src/Init/Data/Nat/Log2.lean @@ -6,7 +6,9 @@ Authors: Gabriel Ebner module prelude -import Init.Data.Nat.Linear +public import Init.Data.Nat.Linear + +public section namespace Nat diff --git a/src/Init/Data/Nat/MinMax.lean b/src/Init/Data/Nat/MinMax.lean index f682da0faa..7a50036c05 100644 --- a/src/Init/Data/Nat/MinMax.lean +++ b/src/Init/Data/Nat/MinMax.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro module prelude -import Init.ByCases +public import Init.ByCases + +public section namespace Nat diff --git a/src/Init/Data/Nat/Mod.lean b/src/Init/Data/Nat/Mod.lean index 9b84da7c1f..366cce004f 100644 --- a/src/Init/Data/Nat/Mod.lean +++ b/src/Init/Data/Nat/Mod.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module prelude -import Init.Omega +public import Init.Omega + +public section /-! # Further results about `mod`. diff --git a/src/Init/Data/Nat/Power2.lean b/src/Init/Data/Nat/Power2.lean index a76d7645ca..4a36825de1 100644 --- a/src/Init/Data/Nat/Power2.lean +++ b/src/Init/Data/Nat/Power2.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Nat.Linear +public import Init.Data.Nat.Linear + +public section namespace Nat diff --git a/src/Init/Data/Nat/SOM.lean b/src/Init/Data/Nat/SOM.lean index 019c466344..c6cff8bba7 100644 --- a/src/Init/Data/Nat/SOM.lean +++ b/src/Init/Data/Nat/SOM.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Nat.Linear -import Init.Data.List.BasicAux +public import Init.Data.Nat.Linear +public import Init.Data.List.BasicAux + +public section namespace Nat.SOM diff --git a/src/Init/Data/Nat/Simproc.lean b/src/Init/Data/Nat/Simproc.lean index 1e5a6ff96c..4120757387 100644 --- a/src/Init/Data/Nat/Simproc.lean +++ b/src/Init/Data/Nat/Simproc.lean @@ -6,9 +6,11 @@ Authors: Joe Hendrix module prelude -import Init.Data.Bool -import Init.Data.Nat.Basic -import Init.Data.Nat.Lemmas +public import Init.Data.Bool +public import Init.Data.Nat.Basic +public import Init.Data.Nat.Lemmas + +public section /-! This contains lemmas used by the Nat simprocs for simplifying arithmetic diff --git a/src/Init/Data/NeZero.lean b/src/Init/Data/NeZero.lean index f424210ced..7e3361253f 100644 --- a/src/Init/Data/NeZero.lean +++ b/src/Init/Data/NeZero.lean @@ -6,7 +6,9 @@ Authors: Eric Rodriguez module prelude -import Init.Data.Zero +public import Init.Data.Zero + +public section /-! diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean index 7b88f40427..38c3132a58 100644 --- a/src/Init/Data/OfScientific.lean +++ b/src/Init/Data/OfScientific.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura module prelude -import Init.Meta -import Init.Data.Float -import Init.Data.Float32 -import Init.Data.Nat.Log2 +public import Init.Meta +public import Init.Data.Float +public import Init.Data.Float32 +public import Init.Data.Nat.Log2 + +public section /-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`). Examples: diff --git a/src/Init/Data/Option.lean b/src/Init/Data/Option.lean index 9dcf625cfd..a025a89f98 100644 --- a/src/Init/Data/Option.lean +++ b/src/Init/Data/Option.lean @@ -6,12 +6,14 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Option.Basic -import Init.Data.Option.BasicAux -import Init.Data.Option.Coe -import Init.Data.Option.Instances -import Init.Data.Option.Lemmas -import Init.Data.Option.Attach -import Init.Data.Option.List -import Init.Data.Option.Monadic -import Init.Data.Option.Array +public import Init.Data.Option.Basic +public import Init.Data.Option.BasicAux +public import Init.Data.Option.Coe +public import Init.Data.Option.Instances +public import Init.Data.Option.Lemmas +public import Init.Data.Option.Attach +public import Init.Data.Option.List +public import Init.Data.Option.Monadic +public import Init.Data.Option.Array + +public section diff --git a/src/Init/Data/Option/Array.lean b/src/Init/Data/Option/Array.lean index cfadebda8f..181bd55601 100644 --- a/src/Init/Data/Option/Array.lean +++ b/src/Init/Data/Option/Array.lean @@ -6,9 +6,11 @@ Authors: Markus Himmel module prelude -import Init.Data.Array.Lemmas -import Init.Data.Option.List -import all Init.Data.Option.Instances +public import Init.Data.Array.Lemmas +public import Init.Data.Option.List +public import all Init.Data.Option.Instances + +public section namespace Option diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean index f7ef2c1f49..6f6d1f4bfd 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -6,12 +6,14 @@ Authors: Kim Morrison module prelude -import Init.Data.Option.Basic -import Init.Data.Option.List -import Init.Data.Option.Array -import Init.Data.Array.Attach -import Init.Data.List.Attach -import Init.BinderPredicates +public import Init.Data.Option.Basic +public import Init.Data.Option.List +public import Init.Data.Option.Array +public import Init.Data.Array.Attach +public import Init.Data.List.Attach +public import Init.BinderPredicates + +public section namespace Option diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index 0356718a66..5aae20258d 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Control.Basic +public import Init.Control.Basic + +public section @[expose] section diff --git a/src/Init/Data/Option/BasicAux.lean b/src/Init/Data/Option/BasicAux.lean index 550367c3b9..63db388b60 100644 --- a/src/Init/Data/Option/BasicAux.lean +++ b/src/Init/Data/Option/BasicAux.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Option.Basic -import Init.Util +public import Init.Data.Option.Basic +public import Init.Util + +public section universe u diff --git a/src/Init/Data/Option/Coe.lean b/src/Init/Data/Option/Coe.lean index 709552522a..b0907aa7a8 100644 --- a/src/Init/Data/Option/Coe.lean +++ b/src/Init/Data/Option/Coe.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Coe +public import Init.Coe + +public section /-! In this file, we define the coercion `α → Option α`. diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean index 2b0ec194b8..a2f3521665 100644 --- a/src/Init/Data/Option/Instances.lean +++ b/src/Init/Data/Option/Instances.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Option.Basic +public import Init.Data.Option.Basic + +public section universe u v diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index 19f1dbdfac..5dc9a6d998 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -6,11 +6,13 @@ Authors: Mario Carneiro module prelude -import all Init.Data.Option.BasicAux -import all Init.Data.Option.Instances -import Init.Data.BEq -import Init.Classical -import Init.Ext +public import all Init.Data.Option.BasicAux +public import all Init.Data.Option.Instances +public import Init.Data.BEq +public import Init.Classical +public import Init.Ext + +public section namespace Option diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean index 604af3787e..94cf3478f0 100644 --- a/src/Init/Data/Option/List.lean +++ b/src/Init/Data/Option/List.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Lemmas -import all Init.Data.List.Control -import all Init.Data.Option.Instances +public import Init.Data.List.Lemmas +public import all Init.Data.List.Control +public import all Init.Data.Option.Instances + +public section namespace Option diff --git a/src/Init/Data/Option/Monadic.lean b/src/Init/Data/Option/Monadic.lean index 5eace2ccda..a297f9fc76 100644 --- a/src/Init/Data/Option/Monadic.lean +++ b/src/Init/Data/Option/Monadic.lean @@ -7,9 +7,11 @@ module prelude -import all Init.Data.Option.Instances -import Init.Data.Option.Attach -import Init.Control.Lawful.Basic +public import all Init.Data.Option.Instances +public import Init.Data.Option.Attach +public import Init.Control.Lawful.Basic + +public section namespace Option diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean index f3b30a1e73..dbb2661962 100644 --- a/src/Init/Data/Ord.lean +++ b/src/Init/Data/Ord.lean @@ -6,10 +6,12 @@ Authors: Dany Fabian, Sebastian Ullrich module prelude -import Init.Data.String.Basic -import Init.Data.Array.Basic -import Init.Data.SInt.Basic -import all Init.Data.Vector.Basic +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 section /-- The result of a comparison according to a total order. diff --git a/src/Init/Data/PLift.lean b/src/Init/Data/PLift.lean index e57df0e20d..d911952b3e 100644 --- a/src/Init/Data/PLift.lean +++ b/src/Init/Data/PLift.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module prelude -import Init.Core +public import Init.Core + +public section deriving instance DecidableEq for PLift diff --git a/src/Init/Data/Prod.lean b/src/Init/Data/Prod.lean index 0f45fd147a..5e733ad2c1 100644 --- a/src/Init/Data/Prod.lean +++ b/src/Init/Data/Prod.lean @@ -6,8 +6,10 @@ Author: Leonardo de Moura module prelude -import Init.SimpLemmas -import Init.NotationExtra +public import Init.SimpLemmas +public import Init.NotationExtra + +public section namespace Prod diff --git a/src/Init/Data/Queue.lean b/src/Init/Data/Queue.lean index bd209c6ccc..ad3d9ab2b6 100644 --- a/src/Init/Data/Queue.lean +++ b/src/Init/Data/Queue.lean @@ -9,7 +9,9 @@ Note: this is only a temporary placeholder. module prelude -import Init.Data.List.Control +public import Init.Data.List.Control + +public section namespace Std diff --git a/src/Init/Data/RArray.lean b/src/Init/Data/RArray.lean index f82cda43dc..307ecf9469 100644 --- a/src/Init/Data/RArray.lean +++ b/src/Init/Data/RArray.lean @@ -7,7 +7,9 @@ Authors: Joachim Breitner module prelude -import Init.PropLemmas +public import Init.PropLemmas + +public section @[expose] section diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index c4b1bf80b3..9b6a545119 100644 --- a/src/Init/Data/Random.lean +++ b/src/Init/Data/Random.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.System.IO +public import Init.System.IO + +public section universe u /-! diff --git a/src/Init/Data/Range.lean b/src/Init/Data/Range.lean index 22fe810b61..ebf0732d69 100644 --- a/src/Init/Data/Range.lean +++ b/src/Init/Data/Range.lean @@ -6,5 +6,7 @@ Authors: Kim Morrison module prelude -import Init.Data.Range.Basic -import Init.Data.Range.Lemmas +public import Init.Data.Range.Basic +public import Init.Data.Range.Lemmas + +public section diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean index de84cc57e7..c8b2e1cc7d 100644 --- a/src/Init/Data/Range/Basic.lean +++ b/src/Init/Data/Range/Basic.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Meta -import Init.Omega +public import Init.Meta +public import Init.Omega + +public section namespace Std -- We put `Range` in `Init` because we want the notation `[i:j]` without importing `Std` diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean index 3dcbae4197..943542a48a 100644 --- a/src/Init/Data/Range/Lemmas.lean +++ b/src/Init/Data/Range/Lemmas.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import all Init.Data.Range.Basic -import Init.Data.List.Range -import Init.Data.List.Monadic -import Init.Data.Nat.Div.Lemmas +public 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 + +public section /-! # Lemmas about `Std.Range` diff --git a/src/Init/Data/Range/Polymorphic.lean b/src/Init/Data/Range/Polymorphic.lean index 9950c5e7f9..9dc63d5eb4 100644 --- a/src/Init/Data/Range/Polymorphic.lean +++ b/src/Init/Data/Range/Polymorphic.lean @@ -6,11 +6,13 @@ Authors: Paul Reichert module prelude -import Init.Data.Range.Polymorphic.Basic -import Init.Data.Range.Polymorphic.Iterators -import Init.Data.Range.Polymorphic.Lemmas -import Init.Data.Range.Polymorphic.Nat -import Init.Data.Range.Polymorphic.NatLemmas +public import Init.Data.Range.Polymorphic.Basic +public import Init.Data.Range.Polymorphic.Iterators +public import Init.Data.Range.Polymorphic.Lemmas +public import Init.Data.Range.Polymorphic.Nat +public import Init.Data.Range.Polymorphic.NatLemmas + +public section /-! # Polymorphic ranges diff --git a/src/Init/Data/Range/Polymorphic/Basic.lean b/src/Init/Data/Range/Polymorphic/Basic.lean index d9552300cc..02f0b333bc 100644 --- a/src/Init/Data/Range/Polymorphic/Basic.lean +++ b/src/Init/Data/Range/Polymorphic/Basic.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Range.Polymorphic.PRange +public import Init.Data.Range.Polymorphic.PRange + +public section namespace Std.PRange diff --git a/src/Init/Data/Range/Polymorphic/Iterators.lean b/src/Init/Data/Range/Polymorphic/Iterators.lean index 80a6a8c84e..3247f2ff28 100644 --- a/src/Init/Data/Range/Polymorphic/Iterators.lean +++ b/src/Init/Data/Range/Polymorphic/Iterators.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Data.Range.Polymorphic.RangeIterator -import Init.Data.Range.Polymorphic.Basic -import Init.Data.Iterators.Combinators.Attach -import Init.Data.Stream +public import Init.Data.Range.Polymorphic.RangeIterator +public import Init.Data.Range.Polymorphic.Basic +public import Init.Data.Iterators.Combinators.Attach +public import Init.Data.Stream + +public section open Std.Iterators diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index 0fc7686c03..d5c90ee75b 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -6,12 +6,14 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators -import Init.Data.Iterators.Lemmas.Consumers.Collect -import all Init.Data.Range.Polymorphic.Basic -import all Init.Data.Range.Polymorphic.RangeIterator -import all Init.Data.Range.Polymorphic.Iterators -import all Init.Data.Iterators.Consumers.Loop +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 section /-! # Lemmas about ranges diff --git a/src/Init/Data/Range/Polymorphic/Nat.lean b/src/Init/Data/Range/Polymorphic/Nat.lean index f6a83b0ae4..80109d0e69 100644 --- a/src/Init/Data/Range/Polymorphic/Nat.lean +++ b/src/Init/Data/Range/Polymorphic/Nat.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import Init.Data.Nat.Lemmas -import Init.Data.Range.Polymorphic.Basic +public import Init.Data.Nat.Lemmas +public import Init.Data.Range.Polymorphic.Basic + +public section namespace Std.PRange diff --git a/src/Init/Data/Range/Polymorphic/NatLemmas.lean b/src/Init/Data/Range/Polymorphic/NatLemmas.lean index 77a6b5a5a3..b1bdfa5a1d 100644 --- a/src/Init/Data/Range/Polymorphic/NatLemmas.lean +++ b/src/Init/Data/Range/Polymorphic/NatLemmas.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import Init.Data.Range.Polymorphic.Nat -import Init.Data.Range.Polymorphic.Lemmas +public import Init.Data.Range.Polymorphic.Nat +public import Init.Data.Range.Polymorphic.Lemmas + +public section namespace Std.PRange.Nat diff --git a/src/Init/Data/Range/Polymorphic/PRange.lean b/src/Init/Data/Range/Polymorphic/PRange.lean index 1ebd6cf3c5..0b19d603bf 100644 --- a/src/Init/Data/Range/Polymorphic/PRange.lean +++ b/src/Init/Data/Range/Polymorphic/PRange.lean @@ -6,8 +6,10 @@ Authors: Paul Reichert module prelude -import Init.Core -import Init.Data.Range.Polymorphic.UpwardEnumerable +public import Init.Core +public import Init.Data.Range.Polymorphic.UpwardEnumerable + +public section namespace Std.PRange diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean index 48eb2d9d7b..e7e15c840d 100644 --- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean +++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean @@ -6,12 +6,14 @@ Authors: Paul Reichert module prelude -import Init.Data.Iterators.Internal.Termination -import Init.Data.Iterators.Consumers.Access -import Init.Data.Iterators.Consumers.Loop -import Init.Data.Iterators.Consumers.Collect -import Init.Data.Range.Polymorphic.PRange -import Init.Data.List.Sublist +public import Init.Data.Iterators.Internal.Termination +public import Init.Data.Iterators.Consumers.Access +public import Init.Data.Iterators.Consumers.Loop +public import Init.Data.Iterators.Consumers.Collect +public import Init.Data.Range.Polymorphic.PRange +public import Init.Data.List.Sublist + +public section /-! # Range iterator diff --git a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean index a2ef3ede4d..d87be19a3f 100644 --- a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean +++ b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Classical -import Init.Core -import Init.Data.Nat.Basic -import Init.Data.Option.Lemmas +public import Init.Classical +public import Init.Core +public import Init.Data.Nat.Basic +public import Init.Data.Option.Lemmas + +public section namespace Std.PRange diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index 8ea382b895..6f1c696481 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -6,7 +6,9 @@ Author: Leonardo de Moura module prelude -import Init.Data.Format.Basic +public import Init.Data.Format.Basic + +public section open Sum Subtype Nat open Std diff --git a/src/Init/Data/SInt.lean b/src/Init/Data/SInt.lean index dcb8d0da8b..efadfdac1f 100644 --- a/src/Init/Data/SInt.lean +++ b/src/Init/Data/SInt.lean @@ -6,11 +6,13 @@ Authors: Henrik Böving module prelude -import Init.Data.SInt.Basic -import Init.Data.SInt.Float -import Init.Data.SInt.Float32 -import Init.Data.SInt.Lemmas -import Init.Data.SInt.Bitwise +public import Init.Data.SInt.Basic +public import Init.Data.SInt.Float +public import Init.Data.SInt.Float32 +public import Init.Data.SInt.Lemmas +public import Init.Data.SInt.Bitwise + +public section /-! This module contains the definitions and basic theory about signed fixed width integer types. diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean index 102bac4964..c40cc80ac8 100644 --- a/src/Init/Data/SInt/Basic.lean +++ b/src/Init/Data/SInt/Basic.lean @@ -6,7 +6,9 @@ Authors: Henrik Böving module prelude -import Init.Data.UInt.Basic +public import Init.Data.UInt.Basic + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/SInt/Bitwise.lean b/src/Init/Data/SInt/Bitwise.lean index 14eed04605..c75ade05df 100644 --- a/src/Init/Data/SInt/Bitwise.lean +++ b/src/Init/Data/SInt/Bitwise.lean @@ -6,12 +6,14 @@ Authors: Markus Himmel module prelude -import all Init.Data.UInt.Basic -import Init.Data.UInt.Bitwise -import all Init.Data.BitVec.Basic -import all Init.Data.BitVec.Lemmas -import all Init.Data.SInt.Basic -import Init.Data.SInt.Lemmas +public 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.SInt.Lemmas + +public section set_option hygiene false in macro "declare_bitwise_int_theorems" typeName:ident bits:term:arg : command => diff --git a/src/Init/Data/SInt/Float.lean b/src/Init/Data/SInt/Float.lean index 069270854e..402d7618bd 100644 --- a/src/Init/Data/SInt/Float.lean +++ b/src/Init/Data/SInt/Float.lean @@ -6,8 +6,10 @@ Authors: Markus Himmel module prelude -import Init.Data.Float -import Init.Data.SInt.Basic +public import Init.Data.Float +public import Init.Data.SInt.Basic + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/SInt/Float32.lean b/src/Init/Data/SInt/Float32.lean index d73fb7dd4a..6f8a9e85d2 100644 --- a/src/Init/Data/SInt/Float32.lean +++ b/src/Init/Data/SInt/Float32.lean @@ -6,8 +6,10 @@ Authors: Markus Himmel module prelude -import Init.Data.Float32 -import Init.Data.SInt.Basic +public import Init.Data.Float32 +public import Init.Data.SInt.Basic + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean index df115ff25a..ff6f1e9d6c 100644 --- a/src/Init/Data/SInt/Lemmas.lean +++ b/src/Init/Data/SInt/Lemmas.lean @@ -6,15 +6,17 @@ Authors: Markus Himmel module prelude -import all Init.Data.Nat.Bitwise.Basic -import all Init.Data.SInt.Basic -import all Init.Data.BitVec.Basic -import Init.Data.BitVec.Lemmas -import Init.Data.BitVec.Bitblast -import Init.Data.Int.LemmasAux -import all Init.Data.UInt.Basic -import Init.Data.UInt.Lemmas -import Init.System.Platform +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.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.Lemmas +public import Init.System.Platform + +public section open Lean in set_option hygiene false in diff --git a/src/Init/Data/Slice.lean b/src/Init/Data/Slice.lean index cd1102591c..6b66394265 100644 --- a/src/Init/Data/Slice.lean +++ b/src/Init/Data/Slice.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Data.Slice.Basic -import Init.Data.Slice.Notation -import Init.Data.Slice.Operations -import Init.Data.Slice.Array +public import Init.Data.Slice.Basic +public import Init.Data.Slice.Notation +public import Init.Data.Slice.Operations +public import Init.Data.Slice.Array + +public section /-! # Polymorphic slices diff --git a/src/Init/Data/Slice/Array.lean b/src/Init/Data/Slice/Array.lean index d6cd9f7d89..a6f259ffb3 100644 --- a/src/Init/Data/Slice/Array.lean +++ b/src/Init/Data/Slice/Array.lean @@ -6,6 +6,8 @@ Authors: Paul Reichert module prelude -import Init.Data.Slice.Array.Basic -import Init.Data.Slice.Array.Iterator -import Init.Data.Slice.Array.Lemmas +public import Init.Data.Slice.Array.Basic +public import Init.Data.Slice.Array.Iterator +public import Init.Data.Slice.Array.Lemmas + +public section diff --git a/src/Init/Data/Slice/Array/Basic.lean b/src/Init/Data/Slice/Array/Basic.lean index 833e849d50..3ac48f55b0 100644 --- a/src/Init/Data/Slice/Array/Basic.lean +++ b/src/Init/Data/Slice/Array/Basic.lean @@ -6,10 +6,12 @@ Authors: Paul Reichert module prelude -import Init.Core -import Init.Data.Array.Subarray -import Init.Data.Slice.Notation -import Init.Data.Range.Polymorphic.Nat +public import Init.Core +public import Init.Data.Array.Subarray +public import Init.Data.Slice.Notation +public import Init.Data.Range.Polymorphic.Nat + +public section /-! This module provides slice notation for array slices (a.k.a. `Subarray`) and implements an iterator diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean index 4c88ca1dbc..f7f808187f 100644 --- a/src/Init/Data/Slice/Array/Iterator.lean +++ b/src/Init/Data/Slice/Array/Iterator.lean @@ -6,14 +6,16 @@ Authors: Paul Reichert module prelude -import Init.Core -import Init.Data.Slice.Array.Basic -import Init.Data.Iterators.Combinators.Attach -import Init.Data.Iterators.Combinators.FilterMap -import all Init.Data.Range.Polymorphic.Basic -import Init.Data.Range.Polymorphic.Nat -import Init.Data.Range.Polymorphic.Iterators -import Init.Data.Slice.Operations +public import Init.Core +public import Init.Data.Slice.Array.Basic +public import Init.Data.Iterators.Combinators.Attach +public import Init.Data.Iterators.Combinators.FilterMap +public 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 + +public section /-! This module provides slice notation for array slices (a.k.a. `Subarray`) and implements an iterator diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index 395ef640fb..f1991e5328 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -6,14 +6,16 @@ Authors: Paul Reichert module prelude -import all Init.Data.Array.Subarray -import all Init.Data.Slice.Array.Basic -import all Init.Data.Slice.Array.Iterator -import all Init.Data.Slice.Operations -import all Init.Data.Range.Polymorphic.Iterators -import Init.Data.Range.Polymorphic.Lemmas -import Init.Data.Slice.Lemmas -import Init.Data.Iterators.Lemmas +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.Range.Polymorphic.Lemmas +public import Init.Data.Slice.Lemmas +public import Init.Data.Iterators.Lemmas + +public section open Std.Iterators Std.PRange diff --git a/src/Init/Data/Slice/Basic.lean b/src/Init/Data/Slice/Basic.lean index 2a485daeef..59a10e637c 100644 --- a/src/Init/Data/Slice/Basic.lean +++ b/src/Init/Data/Slice/Basic.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Core +public import Init.Core + +public section namespace Std.Slice diff --git a/src/Init/Data/Slice/Lemmas.lean b/src/Init/Data/Slice/Lemmas.lean index 61c83b3a11..ba07e47764 100644 --- a/src/Init/Data/Slice/Lemmas.lean +++ b/src/Init/Data/Slice/Lemmas.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import all Init.Data.Slice.Operations +public import all Init.Data.Slice.Operations + +public section namespace Std.Slice diff --git a/src/Init/Data/Slice/Notation.lean b/src/Init/Data/Slice/Notation.lean index 39ec13b81f..5aa9477ba6 100644 --- a/src/Init/Data/Slice/Notation.lean +++ b/src/Init/Data/Slice/Notation.lean @@ -6,7 +6,9 @@ Authors: Paul Reichert module prelude -import Init.Data.Range.Polymorphic.PRange +public import Init.Data.Range.Polymorphic.PRange + +public section /-! # Slice notation diff --git a/src/Init/Data/Slice/Operations.lean b/src/Init/Data/Slice/Operations.lean index 37636e62c7..f6e90ffded 100644 --- a/src/Init/Data/Slice/Operations.lean +++ b/src/Init/Data/Slice/Operations.lean @@ -6,9 +6,11 @@ Authors: Paul Reichert module prelude -import Init.Data.Slice.Basic -import Init.Data.Slice.Notation -import Init.Data.Iterators +public import Init.Data.Slice.Basic +public import Init.Data.Slice.Notation +public import Init.Data.Iterators + +public section open Std.Iterators diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean index a627c8bcd0..f8aaca00fd 100644 --- a/src/Init/Data/Stream.lean +++ b/src/Init/Data/Stream.lean @@ -6,9 +6,12 @@ Authors: Sebastian Ullrich, Andrew Kent, Leonardo de Moura module prelude -import Init.Data.Range -import Init.Data.Array.Subarray -private import Init.Data.Slice.Array.Basic +public import Init.Data.Range +public import Init.Data.Array.Subarray + +import Init.Data.Slice.Array.Basic + +public section /-! Remark: we considered using the following alternative design diff --git a/src/Init/Data/String.lean b/src/Init/Data/String.lean index 462539a0e4..ec0ce25ad9 100644 --- a/src/Init/Data/String.lean +++ b/src/Init/Data/String.lean @@ -6,6 +6,8 @@ Authors: Leonardo de Moura module prelude -import Init.Data.String.Basic -import Init.Data.String.Extra -import Init.Data.String.Lemmas +public import Init.Data.String.Basic +public import Init.Data.String.Extra +public import Init.Data.String.Lemmas + +public section diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index b2f9e36d06..6764c462e7 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -6,8 +6,10 @@ Author: Leonardo de Moura, Mario Carneiro module prelude -import Init.Data.List.Basic -import Init.Data.Char.Basic +public import Init.Data.List.Basic +public import Init.Data.Char.Basic + +public section universe u diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index 7120c9fda8..28638ab329 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import all Init.Data.ByteArray.Basic -import all Init.Data.String.Basic -import Init.Data.UInt.Lemmas +public import all Init.Data.ByteArray.Basic +public import all Init.Data.String.Basic +public import Init.Data.UInt.Lemmas + +public section namespace String diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean index 33c8340fdc..5160feaea3 100644 --- a/src/Init/Data/String/Lemmas.lean +++ b/src/Init/Data/String/Lemmas.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Char.Lemmas -import Init.Data.List.Lex +public import Init.Data.Char.Lemmas +public import Init.Data.List.Lex + +public section namespace String diff --git a/src/Init/Data/Subtype.lean b/src/Init/Data/Subtype.lean index 486b2f33a0..d712eb0b79 100644 --- a/src/Init/Data/Subtype.lean +++ b/src/Init/Data/Subtype.lean @@ -6,8 +6,10 @@ Authors: Johannes Hölzl module prelude -import Init.Ext -import Init.Core +public import Init.Ext +public import Init.Core + +public section namespace Subtype diff --git a/src/Init/Data/Sum.lean b/src/Init/Data/Sum.lean index 69807be6d3..2f6af705e5 100644 --- a/src/Init/Data/Sum.lean +++ b/src/Init/Data/Sum.lean @@ -6,5 +6,7 @@ Authors: Mario Carneiro, Yury G. Kudryashov module prelude -import Init.Data.Sum.Basic -import Init.Data.Sum.Lemmas +public import Init.Data.Sum.Basic +public import Init.Data.Sum.Lemmas + +public section diff --git a/src/Init/Data/Sum/Basic.lean b/src/Init/Data/Sum/Basic.lean index 13b1b9fbdc..80e376532c 100644 --- a/src/Init/Data/Sum/Basic.lean +++ b/src/Init/Data/Sum/Basic.lean @@ -6,7 +6,9 @@ Authors: Mario Carneiro, Yury G. Kudryashov module prelude -import Init.PropLemmas +public import Init.PropLemmas + +public section /-! # Disjoint union of types diff --git a/src/Init/Data/Sum/Lemmas.lean b/src/Init/Data/Sum/Lemmas.lean index 140b67eced..b46fa443c0 100644 --- a/src/Init/Data/Sum/Lemmas.lean +++ b/src/Init/Data/Sum/Lemmas.lean @@ -6,8 +6,10 @@ Authors: Mario Carneiro, Yury G. Kudryashov module prelude -import all Init.Data.Sum.Basic -import Init.Ext +public import all Init.Data.Sum.Basic +public import Init.Ext + +public section /-! # Disjoint union of types diff --git a/src/Init/Data/ToString.lean b/src/Init/Data/ToString.lean index 09ea314884..e504212499 100644 --- a/src/Init/Data/ToString.lean +++ b/src/Init/Data/ToString.lean @@ -6,5 +6,7 @@ Author: Leonardo de Moura module prelude -import Init.Data.ToString.Basic -import Init.Data.ToString.Macro +public import Init.Data.ToString.Basic +public import Init.Data.ToString.Macro + +public section diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean index 75de5ddadd..94ec7fb889 100644 --- a/src/Init/Data/ToString/Basic.lean +++ b/src/Init/Data/ToString/Basic.lean @@ -6,8 +6,10 @@ Author: Leonardo de Moura module prelude -import Init.Data.Repr -import Init.Data.Option.Basic +public import Init.Data.Repr +public import Init.Data.Option.Basic + +public section open Sum Subtype Nat diff --git a/src/Init/Data/ToString/Macro.lean b/src/Init/Data/ToString/Macro.lean index 3c16377932..2618286e15 100644 --- a/src/Init/Data/ToString/Macro.lean +++ b/src/Init/Data/ToString/Macro.lean @@ -6,7 +6,9 @@ Author: Leonardo de Moura module prelude -meta import Init.Meta +public meta import Init.Meta + +public section syntax:max "s!" interpolatedStr(term) : term diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean index 0b6c2f9e0c..0d74665bab 100644 --- a/src/Init/Data/UInt.lean +++ b/src/Init/Data/UInt.lean @@ -6,8 +6,10 @@ Authors: Henrik Böving module prelude -import Init.Data.UInt.BasicAux -import Init.Data.UInt.Basic -import Init.Data.UInt.Log2 -import Init.Data.UInt.Lemmas -import Init.Data.UInt.Bitwise +public import Init.Data.UInt.BasicAux +public import Init.Data.UInt.Basic +public import Init.Data.UInt.Log2 +public import Init.Data.UInt.Lemmas +public import Init.Data.UInt.Bitwise + +public section diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean index 47d66c760b..49580f4020 100644 --- a/src/Init/Data/UInt/Basic.lean +++ b/src/Init/Data/UInt/Basic.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.UInt.BasicAux -import Init.Data.BitVec.Basic +public import Init.Data.UInt.BasicAux +public import Init.Data.BitVec.Basic + +public section set_option linter.missingDocs true diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean index 1dac108b2d..89e555e253 100644 --- a/src/Init/Data/UInt/BasicAux.lean +++ b/src/Init/Data/UInt/BasicAux.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Fin.Basic -import Init.Data.BitVec.BasicAux +public import Init.Data.Fin.Basic +public import Init.Data.BitVec.BasicAux + +public section @[expose] section diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean index f8c7e9ee85..4bf2b30e34 100644 --- a/src/Init/Data/UInt/Bitwise.lean +++ b/src/Init/Data/UInt/Bitwise.lean @@ -6,10 +6,12 @@ Authors: Markus Himmel, Mac Malone module prelude -import all Init.Data.BitVec.Basic -import all Init.Data.UInt.Basic -import Init.Data.UInt.Lemmas -import Init.Data.Fin.Bitwise +public import all Init.Data.BitVec.Basic +public import all Init.Data.UInt.Basic +public import Init.Data.UInt.Lemmas +public import Init.Data.Fin.Bitwise + +public section set_option hygiene false in macro "declare_bitwise_uint_theorems" typeName:ident bits:term:arg : command => diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index 4c263587b5..01da42ee72 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -6,15 +6,17 @@ Authors: Leonardo de Moura, François G. Dorais, Mario Carneiro, Mac Malone, Mar module prelude -import all Init.Data.UInt.Basic -import all Init.Data.UInt.BasicAux -import Init.Data.Fin.Lemmas -import all Init.Data.Fin.Bitwise -import all Init.Data.BitVec.BasicAux -import all Init.Data.BitVec.Basic -import Init.Data.BitVec.Lemmas -import Init.Data.Nat.Div.Lemmas -import Init.System.Platform +public import all Init.Data.UInt.Basic +public 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.BitVec.Lemmas +public import Init.Data.Nat.Div.Lemmas +public import Init.System.Platform + +public section open Lean in set_option hygiene false in diff --git a/src/Init/Data/UInt/Log2.lean b/src/Init/Data/UInt/Log2.lean index 07ed399c18..5b14bfac01 100644 --- a/src/Init/Data/UInt/Log2.lean +++ b/src/Init/Data/UInt/Log2.lean @@ -6,7 +6,9 @@ Authors: Henrik Böving module prelude -import Init.Data.Fin.Log2 +public import Init.Data.Fin.Log2 + +public section /-- Base-two logarithm of 8-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`. diff --git a/src/Init/Data/ULift.lean b/src/Init/Data/ULift.lean index ca26002964..4f7bd00f67 100644 --- a/src/Init/Data/ULift.lean +++ b/src/Init/Data/ULift.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module prelude -import Init.Core +public import Init.Core + +public section deriving instance DecidableEq for ULift diff --git a/src/Init/Data/Vector.lean b/src/Init/Data/Vector.lean index 1c2a83dc1a..1d32b4d739 100644 --- a/src/Init/Data/Vector.lean +++ b/src/Init/Data/Vector.lean @@ -6,19 +6,21 @@ Authors: Kim Morrison module prelude -import Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas -import Init.Data.Vector.Lex -import Init.Data.Vector.MapIdx -import Init.Data.Vector.Count -import Init.Data.Vector.DecidableEq -import Init.Data.Vector.Zip -import Init.Data.Vector.OfFn -import Init.Data.Vector.Range -import Init.Data.Vector.Erase -import Init.Data.Vector.Monadic -import Init.Data.Vector.InsertIdx -import Init.Data.Vector.FinRange -import Init.Data.Vector.Extract -import Init.Data.Vector.Perm -import Init.Data.Vector.Find +public import Init.Data.Vector.Basic +public import Init.Data.Vector.Lemmas +public import Init.Data.Vector.Lex +public import Init.Data.Vector.MapIdx +public import Init.Data.Vector.Count +public import Init.Data.Vector.DecidableEq +public import Init.Data.Vector.Zip +public import Init.Data.Vector.OfFn +public import Init.Data.Vector.Range +public import Init.Data.Vector.Erase +public import Init.Data.Vector.Monadic +public import Init.Data.Vector.InsertIdx +public import Init.Data.Vector.FinRange +public import Init.Data.Vector.Extract +public import Init.Data.Vector.Perm +public import Init.Data.Vector.Find + +public section diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean index efd868408f..b3f89acd76 100644 --- a/src/Init/Data/Vector/Attach.lean +++ b/src/Init/Data/Vector/Attach.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Vector.Lemmas -import all Init.Data.Array.Attach +public import Init.Data.Vector.Lemmas +public import all Init.Data.Array.Attach + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index b20c8cb86e..3701197b8b 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -7,14 +7,16 @@ Authors: Shreyas Srinivas, François G. Dorais, Kim Morrison module prelude -meta import Init.Coe -import Init.Data.Array.Lemmas -import Init.Data.Array.MapIdx -import Init.Data.Array.InsertIdx -import Init.Data.Array.Range -import Init.Data.Range -private import Init.Data.Slice.Array.Basic -import Init.Data.Stream +public meta import Init.Coe +public import Init.Data.Array.Lemmas +public import Init.Data.Array.MapIdx +public import Init.Data.Array.InsertIdx +public import Init.Data.Array.Range +public import Init.Data.Range +import Init.Data.Slice.Array.Basic +public import Init.Data.Stream + +public section /-! # Vectors diff --git a/src/Init/Data/Vector/Count.lean b/src/Init/Data/Vector/Count.lean index 40e6308840..b750d07289 100644 --- a/src/Init/Data/Vector/Count.lean +++ b/src/Init/Data/Vector/Count.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Count -import all Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas +public import all Init.Data.Array.Count +public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Lemmas + +public section /-! # Lemmas about `Vector.countP` and `Vector.count`. diff --git a/src/Init/Data/Vector/DecidableEq.lean b/src/Init/Data/Vector/DecidableEq.lean index 8df8536f51..c79403dd1a 100644 --- a/src/Init/Data/Vector/DecidableEq.lean +++ b/src/Init/Data/Vector/DecidableEq.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Array.DecidableEq -import Init.Data.Vector.Lemmas +public import Init.Data.Array.DecidableEq +public import Init.Data.Vector.Lemmas + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Vector/Erase.lean b/src/Init/Data/Vector/Erase.lean index 509c508726..53bf70922c 100644 --- a/src/Init/Data/Vector/Erase.lean +++ b/src/Init/Data/Vector/Erase.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Vector.Lemmas -import Init.Data.Array.Erase +public import Init.Data.Vector.Lemmas +public import Init.Data.Array.Erase + +public section /-! # Lemmas about `Vector.eraseIdx`. diff --git a/src/Init/Data/Vector/Extract.lean b/src/Init/Data/Vector/Extract.lean index 1ab74156b7..509c0816b5 100644 --- a/src/Init/Data/Vector/Extract.lean +++ b/src/Init/Data/Vector/Extract.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Vector.Lemmas -import Init.Data.Array.Extract +public import Init.Data.Vector.Lemmas +public import Init.Data.Array.Extract + +public section /-! # Lemmas about `Vector.extract` diff --git a/src/Init/Data/Vector/FinRange.lean b/src/Init/Data/Vector/FinRange.lean index 883f6f475c..25c23f7217 100644 --- a/src/Init/Data/Vector/FinRange.lean +++ b/src/Init/Data/Vector/FinRange.lean @@ -6,8 +6,10 @@ Authors: François G. Dorais module prelude -import Init.Data.Array.FinRange -import Init.Data.Vector.OfFn +public import Init.Data.Array.FinRange +public import Init.Data.Vector.OfFn + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean index cbf9df35f3..f65459effc 100644 --- a/src/Init/Data/Vector/Find.lean +++ b/src/Init/Data/Vector/Find.lean @@ -6,12 +6,14 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Basic -import all Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas -import Init.Data.Vector.Attach -import Init.Data.Vector.Range -import Init.Data.Array.Find +public import all Init.Data.Array.Basic +public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Lemmas +public import Init.Data.Vector.Attach +public import Init.Data.Vector.Range +public import Init.Data.Array.Find + +public section /-! # Lemmas about `Vector.findSome?`, `Vector.find?`, `Vector.findFinIdx?`. diff --git a/src/Init/Data/Vector/InsertIdx.lean b/src/Init/Data/Vector/InsertIdx.lean index 18a520fb59..143c5ac6b3 100644 --- a/src/Init/Data/Vector/InsertIdx.lean +++ b/src/Init/Data/Vector/InsertIdx.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Vector.Lemmas -import Init.Data.Array.InsertIdx +public import Init.Data.Vector.Lemmas +public import Init.Data.Array.InsertIdx + +public section /-! # insertIdx diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 6b80491e3b..eabcc8fe1c 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -6,10 +6,12 @@ Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison module prelude -import all Init.Data.Array.Basic -import all Init.Data.Vector.Basic -import Init.Data.Array.Attach -import Init.Data.Array.Find +public import all Init.Data.Array.Basic +public import all Init.Data.Vector.Basic +public import Init.Data.Array.Attach +public import Init.Data.Array.Find + +public section /-! ## Vectors diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index 06cb9100b5..6b7766e8a6 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import all Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas -import all Init.Data.Array.Lex.Basic -import Init.Data.Array.Lex.Lemmas +public 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.Lemmas + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean index e98d8da418..8e62dd6e59 100644 --- a/src/Init/Data/Vector/MapIdx.lean +++ b/src/Init/Data/Vector/MapIdx.lean @@ -6,11 +6,13 @@ Authors: Kim Morrison module prelude -import Init.Data.Array.MapIdx -import all Init.Data.Array.Basic -import all Init.Data.Vector.Basic -import Init.Data.Vector.Attach -import Init.Data.Vector.Lemmas +public import Init.Data.Array.MapIdx +public import all Init.Data.Array.Basic +public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Attach +public import Init.Data.Vector.Lemmas + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index 63bab2e155..246984656b 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/src/Init/Data/Vector/Monadic.lean @@ -6,11 +6,13 @@ Authors: Kim Morrison module prelude -import all Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas -import Init.Data.Vector.Attach -import Init.Data.Array.Monadic -import Init.Control.Lawful.Lemmas +public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Lemmas +public import Init.Data.Vector.Attach +public import Init.Data.Array.Monadic +public import Init.Control.Lawful.Lemmas + +public section /-! # Lemmas about `Vector.forIn'` and `Vector.forIn`. diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean index 609786e645..193e8fe5f1 100644 --- a/src/Init/Data/Vector/OfFn.lean +++ b/src/Init/Data/Vector/OfFn.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import all Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas -import Init.Data.Vector.Monadic -import Init.Data.Array.OfFn +public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Lemmas +public import Init.Data.Vector.Monadic +public import Init.Data.Array.OfFn + +public section /-! # Theorems about `Vector.ofFn` diff --git a/src/Init/Data/Vector/Perm.lean b/src/Init/Data/Vector/Perm.lean index e99bec6f10..4153ebddae 100644 --- a/src/Init/Data/Vector/Perm.lean +++ b/src/Init/Data/Vector/Perm.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Basic -import Init.Data.Array.Perm -import all Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas +public import all Init.Data.Array.Basic +public import Init.Data.Array.Perm +public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Lemmas + +public section set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. diff --git a/src/Init/Data/Vector/Range.lean b/src/Init/Data/Vector/Range.lean index f0f9a57d60..bf8d6f993d 100644 --- a/src/Init/Data/Vector/Range.lean +++ b/src/Init/Data/Vector/Range.lean @@ -6,12 +6,14 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Basic -import all Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas -import Init.Data.Vector.Zip -import Init.Data.Vector.MapIdx -import Init.Data.Array.Range +public import all Init.Data.Array.Basic +public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Lemmas +public import Init.Data.Vector.Zip +public import Init.Data.Vector.MapIdx +public import Init.Data.Array.Range + +public section /-! # Lemmas about `Vector.range'`, `Vector.range`, and `Vector.zipIdx` diff --git a/src/Init/Data/Vector/Zip.lean b/src/Init/Data/Vector/Zip.lean index 7ca89f93cb..13b48eb9d9 100644 --- a/src/Init/Data/Vector/Zip.lean +++ b/src/Init/Data/Vector/Zip.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import all Init.Data.Array.Basic -import Init.Data.Array.Zip -import all Init.Data.Vector.Basic -import Init.Data.Vector.Lemmas +public import all Init.Data.Array.Basic +public import Init.Data.Array.Zip +public import all Init.Data.Vector.Basic +public import Init.Data.Vector.Lemmas + +public section /-! # Lemmas about `Vector.zip`, `Vector.zipWith`, `Vector.zipWithAll`, and `Vector.unzip`. diff --git a/src/Init/Data/Zero.lean b/src/Init/Data/Zero.lean index b6cd68a527..f3908f007d 100644 --- a/src/Init/Data/Zero.lean +++ b/src/Init/Data/Zero.lean @@ -6,7 +6,9 @@ Authors: Gabriel Ebner, Mario Carneiro module prelude -import Init.Core +public import Init.Core + +public section /-! Instances converting between `Zero α` and `OfNat α (nat_lit 0)`. diff --git a/src/Init/Dynamic.lean b/src/Init/Dynamic.lean index 1451eee40d..da91b80e52 100644 --- a/src/Init/Dynamic.lean +++ b/src/Init/Dynamic.lean @@ -7,7 +7,9 @@ Authors: Gabriel Ebner module prelude -import Init.Core +public import Init.Core + +public section open Lean diff --git a/src/Init/Ext.lean b/src/Init/Ext.lean index 1a862876d9..6af6f80086 100644 --- a/src/Init/Ext.lean +++ b/src/Init/Ext.lean @@ -6,9 +6,11 @@ Authors: Gabriel Ebner, Mario Carneiro module prelude -import Init.Data.ToString.Macro -import Init.TacticsExtra -import Init.RCases +public import Init.Data.ToString.Macro +public import Init.TacticsExtra +public import Init.RCases + +public section namespace Lean namespace Parser.Attr diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 4a086b7a2c..9439f920d0 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Util +public import Init.Util + +public section @[expose] section diff --git a/src/Init/Grind.lean b/src/Init/Grind.lean index 02dd3b87bc..8560f88e69 100644 --- a/src/Init/Grind.lean +++ b/src/Init/Grind.lean @@ -6,18 +6,20 @@ Authors: Leonardo de Moura module prelude -import Init.Grind.Norm -import Init.Grind.Tactics -import Init.Grind.Lemmas -import Init.Grind.Cases -import Init.Grind.Propagator -import Init.Grind.Util -import Init.Grind.Offset -import Init.Grind.PP -import Init.Grind.Ring -import Init.Grind.Module -import Init.Grind.Ordered -import Init.Grind.Ext -import Init.Grind.ToInt -import Init.Grind.ToIntLemmas -import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs. +public import Init.Grind.Norm +public import Init.Grind.Tactics +public import Init.Grind.Lemmas +public import Init.Grind.Cases +public import Init.Grind.Propagator +public import Init.Grind.Util +public import Init.Grind.Offset +public import Init.Grind.PP +public import Init.Grind.Ring +public import Init.Grind.Module +public import Init.Grind.Ordered +public import Init.Grind.Ext +public import Init.Grind.ToInt +public import Init.Grind.ToIntLemmas +public import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs. + +public section diff --git a/src/Init/Grind/Cases.lean b/src/Init/Grind/Cases.lean index 8c78fac71e..5f931846ab 100644 --- a/src/Init/Grind/Cases.lean +++ b/src/Init/Grind/Cases.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Core -import Init.Grind.Tactics +public import Init.Core +public import Init.Grind.Tactics + +public section attribute [grind cases eager] And Prod False Empty True PUnit Exists Subtype attribute [grind cases] Or diff --git a/src/Init/Grind/Ext.lean b/src/Init/Grind/Ext.lean index 72aa41888c..03344387ad 100644 --- a/src/Init/Grind/Ext.lean +++ b/src/Init/Grind/Ext.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Ext -import Init.Grind.Tactics +public import Init.Ext +public import Init.Grind.Tactics + +public section attribute [grind ext] funext Prod Subtype Sigma PSigma diff --git a/src/Init/Grind/Lemmas.lean b/src/Init/Grind/Lemmas.lean index 930e02bda3..abfaa21496 100644 --- a/src/Init/Grind/Lemmas.lean +++ b/src/Init/Grind/Lemmas.lean @@ -6,11 +6,13 @@ Authors: Leonardo de Moura module prelude -import Init.Core -import Init.SimpLemmas -import Init.Classical -import Init.ByCases -import Init.Grind.Util +public import Init.Core +public import Init.SimpLemmas +public import Init.Classical +public import Init.ByCases +public import Init.Grind.Util + +public section namespace Lean.Grind diff --git a/src/Init/Grind/Module.lean b/src/Init/Grind/Module.lean index 6add2f1d99..a314e49967 100644 --- a/src/Init/Grind/Module.lean +++ b/src/Init/Grind/Module.lean @@ -6,5 +6,7 @@ Authors: Kim Morrison module prelude -import Init.Grind.Module.Basic -import Init.Grind.Module.Envelope +public import Init.Grind.Module.Basic +public import Init.Grind.Module.Envelope + +public section diff --git a/src/Init/Grind/Module/Basic.lean b/src/Init/Grind/Module/Basic.lean index f80a2fbae6..fd179923fc 100644 --- a/src/Init/Grind/Module/Basic.lean +++ b/src/Init/Grind/Module/Basic.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.Order -import all Init.Grind.ToInt +public import Init.Data.Int.Order +public import all Init.Grind.ToInt + +public section namespace Lean.Grind diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean index 75f5796c88..a03eb6a518 100644 --- a/src/Init/Grind/Module/Envelope.lean +++ b/src/Init/Grind/Module/Envelope.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ordered.Module -import all Init.Data.AC +public import Init.Grind.Ordered.Module +public import all Init.Data.AC + +public section namespace Lean.Grind.IntModule diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean index 239e0d8b9f..b16ad25190 100644 --- a/src/Init/Grind/Norm.lean +++ b/src/Init/Grind/Norm.lean @@ -6,13 +6,15 @@ Authors: Leonardo de Moura module prelude -import Init.SimpLemmas -import Init.PropLemmas -import Init.Classical -import Init.ByCases -import Init.Data.Int.Linear -import Init.Data.Int.Pow -import Init.Grind.Ring.Field +public import Init.SimpLemmas +public import Init.PropLemmas +public import Init.Classical +public import Init.ByCases +public import Init.Data.Int.Linear +public import Init.Data.Int.Pow +public import Init.Grind.Ring.Field + +public section namespace Lean.Grind /-! diff --git a/src/Init/Grind/Offset.lean b/src/Init/Grind/Offset.lean index ee8fcd38c5..12c5e587f2 100644 --- a/src/Init/Grind/Offset.lean +++ b/src/Init/Grind/Offset.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Core -import Init.Omega +public import Init.Core +public import Init.Omega + +public section namespace Lean.Grind abbrev isLt (x y : Nat) : Bool := x < y diff --git a/src/Init/Grind/Ordered.lean b/src/Init/Grind/Ordered.lean index 02f40b17f5..723e2080e5 100644 --- a/src/Init/Grind/Ordered.lean +++ b/src/Init/Grind/Ordered.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ordered.Order -import Init.Grind.Ordered.Module -import Init.Grind.Ordered.Ring -import Init.Grind.Ordered.Field -import Init.Grind.Ordered.Int -import Init.Grind.Ordered.Linarith +public import Init.Grind.Ordered.Order +public import Init.Grind.Ordered.Module +public import Init.Grind.Ordered.Ring +public import Init.Grind.Ordered.Field +public import Init.Grind.Ordered.Int +public import Init.Grind.Ordered.Linarith + +public section diff --git a/src/Init/Grind/Ordered/Field.lean b/src/Init/Grind/Ordered/Field.lean index 560ab9abab..b8157ab5c2 100644 --- a/src/Init/Grind/Ordered/Field.lean +++ b/src/Init/Grind/Ordered/Field.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Field -import Init.Grind.Ordered.Ring +public import Init.Grind.Ring.Field +public import Init.Grind.Ordered.Ring + +public section namespace Lean.Grind diff --git a/src/Init/Grind/Ordered/Int.lean b/src/Init/Grind/Ordered/Int.lean index fbcbe6e356..ef1e5191d6 100644 --- a/src/Init/Grind/Ordered/Int.lean +++ b/src/Init/Grind/Ordered/Int.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ordered.Ring -import Init.GrindInstances.Ring.Int -import Init.Omega +public import Init.Grind.Ordered.Ring +public import Init.GrindInstances.Ring.Int +public import Init.Omega + +public section /-! # `grind` instances for `Int` as an ordered module. diff --git a/src/Init/Grind/Ordered/Linarith.lean b/src/Init/Grind/Ordered/Linarith.lean index d23b97b9b9..badc16e80f 100644 --- a/src/Init/Grind/Ordered/Linarith.lean +++ b/src/Init/Grind/Ordered/Linarith.lean @@ -5,12 +5,14 @@ Authors: Leonardo de Moura -/ module prelude -import Init.Grind.Ordered.Module -import Init.Grind.Ordered.Ring -import Init.Grind.Ring.Field -import all Init.Data.Ord -import all Init.Data.AC -import Init.Data.RArray +public import Init.Grind.Ordered.Module +public import Init.Grind.Ordered.Ring +public import Init.Grind.Ring.Field +public import all Init.Data.Ord +public import all Init.Data.AC +public import Init.Data.RArray + +public section /-! Support for the linear arithmetic module for `IntModule` in `grind` diff --git a/src/Init/Grind/Ordered/Module.lean b/src/Init/Grind/Ordered/Module.lean index 9266f65e86..4716176b1a 100644 --- a/src/Init/Grind/Ordered/Module.lean +++ b/src/Init/Grind/Ordered/Module.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.Order -import Init.Grind.Module.Basic -import Init.Grind.Ordered.Order +public import Init.Data.Int.Order +public import Init.Grind.Module.Basic +public import Init.Grind.Ordered.Order + +public section namespace Lean.Grind diff --git a/src/Init/Grind/Ordered/Order.lean b/src/Init/Grind/Ordered/Order.lean index c732d37bd4..e3e4c06d8c 100644 --- a/src/Init/Grind/Ordered/Order.lean +++ b/src/Init/Grind/Ordered/Order.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.Order +public import Init.Data.Int.Order + +public section namespace Lean.Grind diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean index 12a0cb93e2..295764dbc4 100644 --- a/src/Init/Grind/Ordered/Ring.lean +++ b/src/Init/Grind/Ordered/Ring.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Basic -import Init.Grind.Ordered.Module +public import Init.Grind.Ring.Basic +public import Init.Grind.Ordered.Module + +public section namespace Lean.Grind diff --git a/src/Init/Grind/PP.lean b/src/Init/Grind/PP.lean index 7e2cbf4a1e..9e7adf9b60 100644 --- a/src/Init/Grind/PP.lean +++ b/src/Init/Grind/PP.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.NotationExtra +public import Init.NotationExtra + +public section namespace Lean.Grind /-! diff --git a/src/Init/Grind/Propagator.lean b/src/Init/Grind/Propagator.lean index ae72a6cef7..fc1c1abf49 100644 --- a/src/Init/Grind/Propagator.lean +++ b/src/Init/Grind/Propagator.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.NotationExtra +public import Init.NotationExtra + +public section namespace Lean.Parser diff --git a/src/Init/Grind/Ring.lean b/src/Init/Grind/Ring.lean index 8dce3927c3..99a3330a7a 100644 --- a/src/Init/Grind/Ring.lean +++ b/src/Init/Grind/Ring.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Basic -import Init.Grind.Ring.Poly -import Init.Grind.Ring.Field -import Init.Grind.Ring.Envelope -import Init.Grind.Ring.OfSemiring -import Init.Grind.Ring.ToInt +public import Init.Grind.Ring.Basic +public import Init.Grind.Ring.Poly +public import Init.Grind.Ring.Field +public import Init.Grind.Ring.Envelope +public import Init.Grind.Ring.OfSemiring +public import Init.Grind.Ring.ToInt + +public section diff --git a/src/Init/Grind/Ring/Basic.lean b/src/Init/Grind/Ring/Basic.lean index 58d31c5a38..27a48d999b 100644 --- a/src/Init/Grind/Ring/Basic.lean +++ b/src/Init/Grind/Ring/Basic.lean @@ -6,11 +6,13 @@ Authors: Kim Morrison module prelude -import Init.Data.Zero -import Init.Data.Int.DivMod.Lemmas -import Init.Data.Int.Pow -import Init.TacticsExtra -import Init.Grind.Module.Basic +public import Init.Data.Zero +public import Init.Data.Int.DivMod.Lemmas +public import Init.Data.Int.Pow +public import Init.TacticsExtra +public import Init.Grind.Module.Basic + +public section /-! # A monolithic commutative ring typeclass for internal use in `grind`. diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean index eb2099dbc0..3d08cbce6f 100644 --- a/src/Init/Grind/Ring/Envelope.lean +++ b/src/Init/Grind/Ring/Envelope.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura, Kim Morrison module prelude -import Init.Grind.Ring.Basic -import Init.Grind.Ordered.Ring -import all Init.Data.AC +public import Init.Grind.Ring.Basic +public import Init.Grind.Ordered.Ring +public import all Init.Data.AC + +public section namespace Lean.Grind.Ring diff --git a/src/Init/Grind/Ring/Field.lean b/src/Init/Grind/Ring/Field.lean index 34025004e6..5bc67fdb34 100644 --- a/src/Init/Grind/Ring/Field.lean +++ b/src/Init/Grind/Ring/Field.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Basic +public import Init.Grind.Ring.Basic + +public section namespace Lean.Grind diff --git a/src/Init/Grind/Ring/OfSemiring.lean b/src/Init/Grind/Ring/OfSemiring.lean index c2f205ef61..8362ff633e 100644 --- a/src/Init/Grind/Ring/OfSemiring.lean +++ b/src/Init/Grind/Ring/OfSemiring.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura module prelude -import Init.Grind.Ring.Envelope -import Init.Data.Hashable -import Init.Data.RArray -import all Init.Grind.Ring.Poly +public import Init.Grind.Ring.Envelope +public import Init.Data.Hashable +public import Init.Data.RArray +public import all Init.Grind.Ring.Poly + +public section namespace Lean.Grind.Ring.OfSemiring /-! diff --git a/src/Init/Grind/Ring/Poly.lean b/src/Init/Grind/Ring/Poly.lean index 8c2aba7cda..aeee024c5b 100644 --- a/src/Init/Grind/Ring/Poly.lean +++ b/src/Init/Grind/Ring/Poly.lean @@ -6,13 +6,15 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Nat.Lemmas -import Init.Data.Hashable -import all Init.Data.Ord -import Init.Data.RArray -import Init.Grind.Ring.Basic -import Init.Grind.Ring.Field -import Init.Grind.Ordered.Ring +public import Init.Data.Nat.Lemmas +public import Init.Data.Hashable +public import all Init.Data.Ord +public import Init.Data.RArray +public import Init.Grind.Ring.Basic +public import Init.Grind.Ring.Field +public import Init.Grind.Ordered.Ring + +public section namespace Lean.Grind -- These are no longer global instances, so we need to turn them on here. diff --git a/src/Init/Grind/Ring/ToInt.lean b/src/Init/Grind/Ring/ToInt.lean index 3660b2bd32..eaf184460b 100644 --- a/src/Init/Grind/Ring/ToInt.lean +++ b/src/Init/Grind/Ring/ToInt.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Basic -import Init.Grind.ToInt +public import Init.Grind.Ring.Basic +public import Init.Grind.ToInt + +public section namespace Lean.Grind diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 73d5c65d93..4a0a4fdac1 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Tactics +public import Init.Tactics + +public section namespace Lean.Grind /-- diff --git a/src/Init/Grind/ToInt.lean b/src/Init/Grind/ToInt.lean index be64922da4..9d5ef38b49 100644 --- a/src/Init/Grind/ToInt.lean +++ b/src/Init/Grind/ToInt.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.DivMod.Lemmas +public import Init.Data.Int.DivMod.Lemmas + +public section /-! # Typeclasses for types that can be embedded into an interval of `Int`. diff --git a/src/Init/Grind/ToIntLemmas.lean b/src/Init/Grind/ToIntLemmas.lean index 4e2263db8a..893ee13b38 100644 --- a/src/Init/Grind/ToIntLemmas.lean +++ b/src/Init/Grind/ToIntLemmas.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import all Init.Grind.ToInt +public import all Init.Grind.ToInt + +public section namespace Lean.Grind.ToInt diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean index 06320cebf3..64a03d37d4 100644 --- a/src/Init/Grind/Util.lean +++ b/src/Init/Grind/Util.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Core -import Init.Classical +public import Init.Core +public import Init.Classical + +public section namespace Lean.Grind diff --git a/src/Init/GrindInstances.lean b/src/Init/GrindInstances.lean index d48f26f512..81aba4ad54 100644 --- a/src/Init/GrindInstances.lean +++ b/src/Init/GrindInstances.lean @@ -6,6 +6,8 @@ Authors: Kim Morrison module prelude -import Init.GrindInstances.ToInt -import Init.GrindInstances.Ring -import Init.GrindInstances.Nat +public import Init.GrindInstances.ToInt +public import Init.GrindInstances.Ring +public import Init.GrindInstances.Nat + +public section diff --git a/src/Init/GrindInstances/Nat.lean b/src/Init/GrindInstances/Nat.lean index b6c6193ea8..44afac98bc 100644 --- a/src/Init/GrindInstances/Nat.lean +++ b/src/Init/GrindInstances/Nat.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ordered.Module -import Init.Grind.Ring.Basic +public import Init.Grind.Ordered.Module +public import Init.Grind.Ring.Basic + +public section namespace Lean.Grind diff --git a/src/Init/GrindInstances/Ring.lean b/src/Init/GrindInstances/Ring.lean index c34926c06d..b7ca05daa8 100644 --- a/src/Init/GrindInstances/Ring.lean +++ b/src/Init/GrindInstances/Ring.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.GrindInstances.Ring.Nat -import Init.GrindInstances.Ring.Int -import Init.GrindInstances.Ring.UInt -import Init.GrindInstances.Ring.SInt -import Init.GrindInstances.Ring.Fin -import Init.GrindInstances.Ring.BitVec +public import Init.GrindInstances.Ring.Nat +public import Init.GrindInstances.Ring.Int +public import Init.GrindInstances.Ring.UInt +public import Init.GrindInstances.Ring.SInt +public import Init.GrindInstances.Ring.Fin +public import Init.GrindInstances.Ring.BitVec + +public section diff --git a/src/Init/GrindInstances/Ring/BitVec.lean b/src/Init/GrindInstances/Ring/BitVec.lean index 9e6f8a8e44..1ea8c5127f 100644 --- a/src/Init/GrindInstances/Ring/BitVec.lean +++ b/src/Init/GrindInstances/Ring/BitVec.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Basic -import Init.GrindInstances.ToInt -import all Init.Data.BitVec.Basic -import all Init.Grind.ToInt +public import Init.Grind.Ring.Basic +public import Init.GrindInstances.ToInt +public import all Init.Data.BitVec.Basic +public import all Init.Grind.ToInt + +public section namespace Lean.Grind diff --git a/src/Init/GrindInstances/Ring/Fin.lean b/src/Init/GrindInstances/Ring/Fin.lean index 68e7f50903..9dd24c3427 100644 --- a/src/Init/GrindInstances/Ring/Fin.lean +++ b/src/Init/GrindInstances/Ring/Fin.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura module prelude -import all Init.Data.Zero -import Init.Grind.Ring.Basic -import all Init.GrindInstances.ToInt -import Init.Data.Fin.Lemmas +public import all Init.Data.Zero +public import Init.Grind.Ring.Basic +public import all Init.GrindInstances.ToInt +public import Init.Data.Fin.Lemmas + +public section namespace Lean.Grind diff --git a/src/Init/GrindInstances/Ring/Int.lean b/src/Init/GrindInstances/Ring/Int.lean index a5b8c466a4..881b16c4c3 100644 --- a/src/Init/GrindInstances/Ring/Int.lean +++ b/src/Init/GrindInstances/Ring/Int.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Basic -import Init.Data.Int.Lemmas +public import Init.Grind.Ring.Basic +public import Init.Data.Int.Lemmas + +public section namespace Lean.Grind diff --git a/src/Init/GrindInstances/Ring/Nat.lean b/src/Init/GrindInstances/Ring/Nat.lean index f91546ac1a..49e0ba66c6 100644 --- a/src/Init/GrindInstances/Ring/Nat.lean +++ b/src/Init/GrindInstances/Ring/Nat.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ordered.Ring -import Init.Data.Int.Lemmas +public import Init.Grind.Ordered.Ring +public import Init.Data.Int.Lemmas + +public section namespace Lean.Grind diff --git a/src/Init/GrindInstances/Ring/SInt.lean b/src/Init/GrindInstances/Ring/SInt.lean index 8d53e1bc53..34dc2e9bc3 100644 --- a/src/Init/GrindInstances/Ring/SInt.lean +++ b/src/Init/GrindInstances/Ring/SInt.lean @@ -6,12 +6,14 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Basic -import all Init.Grind.ToInt -import Init.GrindInstances.ToInt -import all Init.Data.BitVec.Basic -import all Init.Data.SInt.Basic -import Init.Data.SInt.Lemmas +public import Init.Grind.Ring.Basic +public 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.SInt.Lemmas + +public section namespace Lean.Grind diff --git a/src/Init/GrindInstances/Ring/UInt.lean b/src/Init/GrindInstances/Ring/UInt.lean index f52e7ba336..9b1eab5a32 100644 --- a/src/Init/GrindInstances/Ring/UInt.lean +++ b/src/Init/GrindInstances/Ring/UInt.lean @@ -6,10 +6,12 @@ Authors: Kim Morrison module prelude -import Init.Grind.Ring.Basic -import all Init.GrindInstances.ToInt -import all Init.Data.UInt.Basic -import Init.Data.UInt.Lemmas +public import Init.Grind.Ring.Basic +public import all Init.GrindInstances.ToInt +public import all Init.Data.UInt.Basic +public import Init.Data.UInt.Lemmas + +public section namespace UInt8 diff --git a/src/Init/GrindInstances/ToInt.lean b/src/Init/GrindInstances/ToInt.lean index 7f81a5d0e6..83c5a46e57 100644 --- a/src/Init/GrindInstances/ToInt.lean +++ b/src/Init/GrindInstances/ToInt.lean @@ -6,15 +6,17 @@ Authors: Kim Morrison module prelude -import all Init.Grind.ToInt -import Init.Grind.Module.Basic -import Init.Grind.Ring.ToInt -import Init.Data.Int.DivMod.Basic -import Init.Data.Int.Lemmas -import Init.Data.Int.Order -import Init.Data.Fin.Lemmas -import Init.Data.UInt.Lemmas -import Init.Data.SInt.Lemmas +public import all Init.Grind.ToInt +public import Init.Grind.Module.Basic +public import Init.Grind.Ring.ToInt +public import Init.Data.Int.DivMod.Basic +public import Init.Data.Int.Lemmas +public import Init.Data.Int.Order +public import Init.Data.Fin.Lemmas +public import Init.Data.UInt.Lemmas +public import Init.Data.SInt.Lemmas + +public section namespace Lean.Grind diff --git a/src/Init/Guard.lean b/src/Init/Guard.lean index 6c722439d5..a018f441a2 100644 --- a/src/Init/Guard.lean +++ b/src/Init/Guard.lean @@ -6,9 +6,11 @@ Authors: Mario Carneiro module prelude -import Init.Tactics -import Init.Conv -import Init.NotationExtra +public import Init.Tactics +public import Init.Conv +public import Init.NotationExtra + +public section namespace Lean.Parser diff --git a/src/Init/Hints.lean b/src/Init/Hints.lean index 2d314d7340..eeeb822cbf 100644 --- a/src/Init/Hints.lean +++ b/src/Init/Hints.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.NotationExtra +public import Init.NotationExtra + +public section /- Hint for making sure `Not p` is definitionally equal to `p → False` even when `TransparencyMode.reducible` -/ diff --git a/src/Init/Internal.lean b/src/Init/Internal.lean index d4beb95f76..c15228a716 100644 --- a/src/Init/Internal.lean +++ b/src/Init/Internal.lean @@ -6,7 +6,9 @@ Authors: Joachim Breitner module prelude -import Init.Internal.Order +public import Init.Internal.Order + +public section /-! This directory is used for components of the standard library that are either considered diff --git a/src/Init/Internal/Order.lean b/src/Init/Internal/Order.lean index 47e5bda942..d14bfd6884 100644 --- a/src/Init/Internal/Order.lean +++ b/src/Init/Internal/Order.lean @@ -6,6 +6,8 @@ Authors: Joachim Breitner module prelude -import Init.Internal.Order.Basic -import Init.Internal.Order.Lemmas -import Init.Internal.Order.Tactic +public import Init.Internal.Order.Basic +public import Init.Internal.Order.Lemmas +public import Init.Internal.Order.Tactic + +public section diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index ebc1ecf7da..7466a9dace 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -7,9 +7,11 @@ module prelude -import Init.ByCases -import Init.RCases -import all Init.Control.Except -- for `MonoBind` instance +public import Init.ByCases +public import Init.RCases +public import all Init.Control.Except -- for `MonoBind` instance + +public section /-! This module contains some basic definitions and results from domain theory, intended to be used as diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean index dbdfd1cf21..9b1b6cb3bf 100644 --- a/src/Init/Internal/Order/Lemmas.lean +++ b/src/Init/Internal/Order/Lemmas.lean @@ -8,10 +8,12 @@ module prelude -import all Init.Data.List.Control -import all Init.Data.Option.Basic -import all Init.Data.Array.Basic -import Init.Internal.Order.Basic +public import all Init.Data.List.Control +public import all Init.Data.Option.Basic +public import all Init.Data.Array.Basic +public import Init.Internal.Order.Basic + +public section /-! diff --git a/src/Init/Internal/Order/Tactic.lean b/src/Init/Internal/Order/Tactic.lean index b90da099a6..c83fcacebb 100644 --- a/src/Init/Internal/Order/Tactic.lean +++ b/src/Init/Internal/Order/Tactic.lean @@ -7,7 +7,9 @@ Authors: Joachim Breitner module prelude -import Init.Notation +public import Init.Notation + +public section namespace Lean.Order /-- diff --git a/src/Init/MacroTrace.lean b/src/Init/MacroTrace.lean index 093ff10850..e22f5704f7 100644 --- a/src/Init/MacroTrace.lean +++ b/src/Init/MacroTrace.lean @@ -9,8 +9,10 @@ Extra notation that depends on Init/Meta module prelude -import Init.Data.ToString.Macro -import Init.Meta +public import Init.Data.ToString.Macro +public import Init.Meta + +public section namespace Lean diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 687682fe22..0aba154252 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -8,13 +8,15 @@ Additional goodies for writing macros module prelude -import all Init.Prelude -- for unfolding `Name.beq` -import Init.MetaTypes -import Init.Syntax -import Init.Data.Array.GetLit -import Init.Data.Option.BasicAux -meta import Init.Data.Array.Basic -meta import Init.Syntax +public import all Init.Prelude -- for unfolding `Name.beq` +public import Init.MetaTypes +public import Init.Syntax +public import Init.Data.Array.GetLit +public import Init.Data.Option.BasicAux +public meta import Init.Data.Array.Basic +public meta import Init.Syntax + +public section namespace Lean diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 24736213b1..a410360e09 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Core +public import Init.Core + +public section namespace Lean diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index aa3071b4c3..a2e0d3532b 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -8,7 +8,9 @@ Notation for operators defined at Prelude.lean module prelude -import Init.Coe +public import Init.Coe + +public section set_option linter.missingDocs true -- keep it documented namespace Lean diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 4ab593467c..747efa4256 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -8,11 +8,13 @@ Extra notation that depends on Init/Meta module prelude -import Init.Data.ToString.Basic -import Init.Conv -import Init.Meta -import Init.While -meta import Init.Data.Option.Basic +public import Init.Data.ToString.Basic +public import Init.Conv +public import Init.Meta +public import Init.While +public meta import Init.Data.Option.Basic + +public section namespace Lean diff --git a/src/Init/Omega.lean b/src/Init/Omega.lean index 786e95e347..d39790a10c 100644 --- a/src/Init/Omega.lean +++ b/src/Init/Omega.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Omega.Int -import Init.Omega.IntList -import Init.Omega.LinearCombo -import Init.Omega.Constraint -import Init.Omega.Logic +public import Init.Omega.Int +public import Init.Omega.IntList +public import Init.Omega.LinearCombo +public import Init.Omega.Constraint +public import Init.Omega.Logic + +public section diff --git a/src/Init/Omega/Coeffs.lean b/src/Init/Omega/Coeffs.lean index b6edd70f62..848b6ddf2a 100644 --- a/src/Init/Omega/Coeffs.lean +++ b/src/Init/Omega/Coeffs.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module prelude -import all Init.Omega.IntList +public import all Init.Omega.IntList + +public section /-! # `Coeffs` as a wrapper for `IntList` diff --git a/src/Init/Omega/Constraint.lean b/src/Init/Omega/Constraint.lean index d8c1a74dce..651dd2c47b 100644 --- a/src/Init/Omega/Constraint.lean +++ b/src/Init/Omega/Constraint.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Omega.LinearCombo -import Init.Omega.Int +public import Init.Omega.LinearCombo +public import Init.Omega.Int + +public section /-! A `Constraint` consists of an optional lower and upper bound (inclusive), diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean index d153e939d4..b8da2152a2 100644 --- a/src/Init/Omega/Int.lean +++ b/src/Init/Omega/Int.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Data.Int.DivMod.Bootstrap -import Init.Data.Int.Order +public import Init.Data.Int.DivMod.Bootstrap +public import Init.Data.Int.Order + +public section /-! # Lemmas about `Nat`, `Int`, and `Fin` needed internally by `omega`. diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean index a94cb51713..b4b914de47 100644 --- a/src/Init/Omega/IntList.lean +++ b/src/Init/Omega/IntList.lean @@ -6,9 +6,11 @@ Authors: Kim Morrison module prelude -import Init.Data.List.Zip -import Init.Data.Int.DivMod.Bootstrap -import Init.Data.Nat.Gcd +public import Init.Data.List.Zip +public import Init.Data.Int.DivMod.Bootstrap +public import Init.Data.Nat.Gcd + +public section @[expose] section diff --git a/src/Init/Omega/LinearCombo.lean b/src/Init/Omega/LinearCombo.lean index 792ebb7a84..f95c0f863f 100644 --- a/src/Init/Omega/LinearCombo.lean +++ b/src/Init/Omega/LinearCombo.lean @@ -6,8 +6,10 @@ Authors: Kim Morrison module prelude -import Init.Omega.Coeffs -import Init.Data.ToString.Macro +public import Init.Omega.Coeffs +public import Init.Data.ToString.Macro + +public section /-! # Linear combinations diff --git a/src/Init/Omega/Logic.lean b/src/Init/Omega/Logic.lean index 998e2b2517..4cbd75995b 100644 --- a/src/Init/Omega/Logic.lean +++ b/src/Init/Omega/Logic.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module prelude -import Init.PropLemmas +public import Init.PropLemmas + +public section /-! # Specializations of basic logic lemmas diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index ef0b40739d..e9f5511a0c 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -6,6 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -- Don't import Init, because we're in Init itself + +public section set_option linter.missingDocs true -- keep it documented @[expose] section -- Expose all defs @@ -476,7 +478,7 @@ type, and casting `a` across the equality yields `b`, and vice versa. You should avoid using this type if you can. Heterogeneous equality does not have all the same properties as `Eq`, because the assumption that the types of `a` and `b` are equal is often too weak to prove theorems of interest. One -important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y` +public important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y` and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`. (This does follow if you have `f = g` instead.) However if `a` and `b` have the same type then `a = b` and `a ≍ b` are equivalent. @@ -592,7 +594,7 @@ theorem Or.neg_resolve_right (h : Or a (Not b)) (nb : b) : a := h.elim id (absur The Boolean values, `true` and `false`. Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is -important for programming: both propositions and their proofs are erased in the code generator, +public important for programming: both propositions and their proofs are erased in the code generator, while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one bit of run-time information. -/ diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index ac200680c0..c102be7051 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -9,8 +9,10 @@ needed for Core and SimpLemmas. module prelude -import Init.Core -import Init.NotationExtra +public import Init.Core +public import Init.NotationExtra + +public section set_option linter.missingDocs true -- keep it documented /-! ## cast and equality -/ diff --git a/src/Init/RCases.lean b/src/Init/RCases.lean index 2429e9c6ba..8d69422be2 100644 --- a/src/Init/RCases.lean +++ b/src/Init/RCases.lean @@ -6,8 +6,10 @@ Authors: Mario Carneiro, Jacob von Raumer module prelude -import Init.Tactics -import Init.Meta +public import Init.Tactics +public import Init.Meta + +public section /-! diff --git a/src/Init/ShareCommon.lean b/src/Init/ShareCommon.lean index d25450ecac..2441052792 100644 --- a/src/Init/ShareCommon.lean +++ b/src/Init/ShareCommon.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Util -import Init.Data.UInt.Basic +public import Init.Util +public import Init.Data.UInt.Basic + +public section namespace ShareCommon /- diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 9f04331fb0..2342e21cfb 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -8,7 +8,9 @@ notation, basic datatypes and type classes module prelude -import Init.Core +public import Init.Core + +public section set_option linter.missingDocs true -- keep it documented theorem of_eq_true (h : p = True) : p := h ▸ trivial diff --git a/src/Init/Simproc.lean b/src/Init/Simproc.lean index 066492f1c7..8f56dcfb8d 100644 --- a/src/Init/Simproc.lean +++ b/src/Init/Simproc.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.NotationExtra +public import Init.NotationExtra + +public section namespace Lean.Parser /-- diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean index 6ba15cd457..ee5c00e984 100644 --- a/src/Init/SizeOf.lean +++ b/src/Init/SizeOf.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Tactics +public import Init.Tactics + +public section set_option linter.missingDocs true -- keep it documented /-! # SizeOf -/ diff --git a/src/Init/SizeOfLemmas.lean b/src/Init/SizeOfLemmas.lean index 3a07463454..22fe959295 100644 --- a/src/Init/SizeOfLemmas.lean +++ b/src/Init/SizeOfLemmas.lean @@ -6,10 +6,12 @@ Authors: Leonardo de Moura module prelude -import all Init.Data.Char.Basic -import Init.Meta -import all Init.SizeOf -import Init.Data.Nat.Linear +public import all Init.Data.Char.Basic +public import Init.Meta +public import all Init.SizeOf +public import Init.Data.Nat.Linear + +public section @[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by cases a; simp +arith diff --git a/src/Init/Syntax.lean b/src/Init/Syntax.lean index 368a54c9c2..4e2b14f531 100644 --- a/src/Init/Syntax.lean +++ b/src/Init/Syntax.lean @@ -7,7 +7,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Data.Array.Set +public import Init.Data.Array.Set + +public section /-! # Helper functions for `Syntax`. diff --git a/src/Init/System.lean b/src/Init/System.lean index 097803f436..923e3b2bd1 100644 --- a/src/Init/System.lean +++ b/src/Init/System.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.System.IO -import Init.System.Platform -import Init.System.Uri -import Init.System.Mutex -import Init.System.Promise +public import Init.System.IO +public import Init.System.Platform +public import Init.System.Uri +public import Init.System.Mutex +public import Init.System.Promise + +public section diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean index 92fa9d4f91..9cfbed80f1 100644 --- a/src/Init/System/FilePath.lean +++ b/src/Init/System/FilePath.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura, Sebastian Ullrich module prelude -import Init.System.Platform -import Init.Data.ToString.Basic +public import Init.System.Platform +public import Init.Data.ToString.Basic + +public section namespace System open Platform diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index c487dc1b54..c0fa57924a 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -6,11 +6,13 @@ Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Ma module prelude -import Init.System.IOError -import Init.System.FilePath -import Init.System.ST -import Init.Data.Ord -import Init.Data.String.Extra +public import Init.System.IOError +public import Init.System.FilePath +public import Init.System.ST +public import Init.Data.Ord +public import Init.Data.String.Extra + +public section open System diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean index baa85d312e..6c922d80c7 100644 --- a/src/Init/System/IOError.lean +++ b/src/Init/System/IOError.lean @@ -7,7 +7,9 @@ Authors: Simon Hudon module prelude -import Init.Data.ToString.Basic +public import Init.Data.ToString.Basic + +public section /-- Exceptions that may be thrown in the `IO` monad. diff --git a/src/Init/System/Mutex.lean b/src/Init/System/Mutex.lean index fdcff97926..0e0b1a1e4f 100644 --- a/src/Init/System/Mutex.lean +++ b/src/Init/System/Mutex.lean @@ -6,8 +6,10 @@ Authors: Gabriel Ebner module prelude -import Init.System.IO -import Init.Control.StateRef +public import Init.System.IO +public import Init.Control.StateRef + +public section set_option linter.deprecated false diff --git a/src/Init/System/Platform.lean b/src/Init/System/Platform.lean index 5681a27398..25f6116685 100644 --- a/src/Init/System/Platform.lean +++ b/src/Init/System/Platform.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.Nat.Basic -import Init.Data.String.Basic +public import Init.Data.Nat.Basic +public import Init.Data.String.Basic + +public section namespace System namespace Platform diff --git a/src/Init/System/Promise.lean b/src/Init/System/Promise.lean index 59c97351b8..eb938b4b41 100644 --- a/src/Init/System/Promise.lean +++ b/src/Init/System/Promise.lean @@ -6,7 +6,9 @@ Authors: Gabriel Ebner module prelude -import Init.System.IO +public import Init.System.IO + +public section set_option linter.missingDocs true diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean index 3f16e86ddb..77451553c9 100644 --- a/src/Init/System/ST.lean +++ b/src/Init/System/ST.lean @@ -6,9 +6,11 @@ Authors: Leonardo de Moura module prelude -import Init.Classical -import Init.Control.EState -import Init.Control.Reader +public import Init.Classical +public import Init.Control.EState +public import Init.Control.Reader + +public section /-- A restricted version of `IO` in which mutable state and exceptions are the only side effects. diff --git a/src/Init/System/Uri.lean b/src/Init/System/Uri.lean index 8ea32db8b0..b218754a96 100644 --- a/src/Init/System/Uri.lean +++ b/src/Init/System/Uri.lean @@ -6,9 +6,11 @@ Authors: Chris Lovett module prelude -import Init.Data.String.Extra -import Init.Data.Nat.Linear -import Init.System.FilePath +public import Init.Data.String.Extra +public import Init.Data.Nat.Linear +public import Init.System.FilePath + +public section namespace System namespace Uri diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 8fcb1e7dc2..2d1b071eba 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Notation +public import Init.Notation + +public section set_option linter.missingDocs true -- keep it documented namespace Lean.Parser.Tactic diff --git a/src/Init/TacticsExtra.lean b/src/Init/TacticsExtra.lean index b4736179bf..1ccbe8ff25 100644 --- a/src/Init/TacticsExtra.lean +++ b/src/Init/TacticsExtra.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura, Mario Carneiro module prelude -import Init.Tactics -import Init.NotationExtra +public import Init.Tactics +public import Init.NotationExtra + +public section /-! Extra tactics and implementation for some tactics defined at `Init/Tactic.lean` diff --git a/src/Init/Task.lean b/src/Init/Task.lean index 8f99e4bba5..d559183db1 100644 --- a/src/Init/Task.lean +++ b/src/Init/Task.lean @@ -8,8 +8,10 @@ Additional `Task` definitions. module prelude -import Init.Core -import Init.Data.List.Basic +public import Init.Core +public import Init.Data.List.Basic + +public section namespace Task diff --git a/src/Init/Try.lean b/src/Init/Try.lean index 9e23477a67..3597174f2f 100644 --- a/src/Init/Try.lean +++ b/src/Init/Try.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Tactics +public import Init.Tactics + +public section namespace Lean.Try /-- diff --git a/src/Init/Util.lean b/src/Init/Util.lean index 3e575a9e0b..2e2b867356 100644 --- a/src/Init/Util.lean +++ b/src/Init/Util.lean @@ -6,8 +6,10 @@ Authors: Leonardo de Moura module prelude -import Init.Data.String.Basic -import Init.Data.ToString.Basic +public import Init.Data.String.Basic +public import Init.Data.ToString.Basic + +public section universe u v diff --git a/src/Init/WF.lean b/src/Init/WF.lean index 477ffb04a8..28f98a6288 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import Init.SizeOf -import Init.BinderNameHint -import Init.Data.Nat.Basic +public import Init.SizeOf +public import Init.BinderNameHint +public import Init.Data.Nat.Basic + +public section @[expose] section diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index 84a7c2ce1e..59cfbeecea 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -6,9 +6,11 @@ Author: Leonardo de Moura module prelude -import Init.SizeOf -import Init.MetaTypes -import Init.WF +public import Init.SizeOf +public import Init.MetaTypes +public import Init.WF + +public section /-- Unfold definitions commonly used in well founded relation definitions. diff --git a/src/Init/While.lean b/src/Init/While.lean index 726593d632..4d59c5b28d 100644 --- a/src/Init/While.lean +++ b/src/Init/While.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura module prelude -import Init.Core +public import Init.Core + +public section /-! # Notation for `while` and `repeat` loops. diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 198a884aab..d508660084 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -27,13 +27,14 @@ namespace Lean.Elab.Command | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}" private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name) - (isNoncomputable : Bool := false) (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) : + (isNoncomputable isPublic : Bool := false) (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) : CommandElabM Unit := do modify fun s => { s with env := s.env.registerNamespace newNamespace, scopes := { s.scopes.head! with header := header, currNamespace := newNamespace isNoncomputable := s.scopes.head!.isNoncomputable || isNoncomputable + isPublic := s.scopes.head!.isPublic || isPublic attrs := s.scopes.head!.attrs ++ attrs } :: s.scopes } @@ -41,7 +42,7 @@ private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : N if isNewNamespace then activateScoped newNamespace -private def addScopes (header : Name) (isNewNamespace : Bool) (isNoncomputable : Bool := false) +private def addScopes (header : Name) (isNewNamespace : Bool) (isNoncomputable isPublic : Bool := false) (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) : CommandElabM Unit := go header where go @@ -49,7 +50,7 @@ where go | .str p header => do go p let currNamespace ← getCurrNamespace - addScope isNewNamespace header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace) isNoncomputable attrs + addScope isNewNamespace header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace) isNoncomputable isPublic attrs | _ => throwError "invalid scope" private def addNamespace (header : Name) : CommandElabM Unit := @@ -93,9 +94,9 @@ private def checkEndHeader : Name → List Scope → Option Name else pure [] if let some header := header? then - addScopes (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (attrs := attrs) header.getId + addScopes (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (attrs := attrs) header.getId else - addScope (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (attrs := attrs) "" (← getCurrNamespace) + addScope (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (attrs := attrs) "" (← getCurrNamespace) | _ => throwUnsupportedSyntax /-- diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 1522d46e14..9078e74e8d 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -74,6 +74,7 @@ structure Scope where so all sections and namespaces nested within a `noncomputable` section also have this flag set. -/ isNoncomputable : Bool := false + isPublic : Bool := false /-- Attributes that should be applied to all matching declaration in the section. Inherited from parent scopes. @@ -157,7 +158,7 @@ instance : MonadExceptOf Exception CommandElabM where def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := { env := env messages := messages - scopes := [{ header := "", opts := opts }] + scopes := [{ header := "", opts }] maxRecDepth := maxRecDepth.get opts -- Outside of declarations, fall back to a module-specific prefix auxDeclNGen := { namePrefix := mkPrivateName env .anonymous } diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 9dc6e3d2c4..ecf8812db4 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -42,7 +42,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo /-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/ inductive Visibility where - | regular | «protected» | «private» + | regular | «protected» | «private» | «public» deriving Inhabited instance : ToString Visibility where @@ -50,6 +50,22 @@ instance : ToString Visibility where | .regular => "regular" | .private => "private" | .protected => "protected" + | .public => "public" + +def Visibility.isPrivate : Visibility → Bool + | .private => true + | _ => false + +def Visibility.isProtected : Visibility → Bool + | .protected => true + | _ => false + +def Visibility.isPublic : Visibility → Bool + | .public => true + | _ => false + +def Visibility.isInferredPublic (env : Environment) (v : Visibility) : Bool := + if env.isExporting || !env.header.isModule then !v.isPrivate else v.isPublic /-- Whether a declaration is default, partial or nonrec. -/ inductive RecKind where @@ -73,13 +89,11 @@ structure Modifiers where attrs : Array Attribute := #[] deriving Inhabited -def Modifiers.isPrivate : Modifiers → Bool - | { visibility := .private, .. } => true - | _ => false - -def Modifiers.isProtected : Modifiers → Bool - | { visibility := .protected, .. } => true - | _ => false +def Modifiers.isPrivate (m : Modifiers) : Bool := m.visibility.isPrivate +def Modifiers.isProtected (m : Modifiers) : Bool := m.visibility.isProtected +def Modifiers.isPublic (m : Modifiers) : Bool := m.visibility.isPublic +def Modifiers.isInferredPublic (env : Environment) (m : Modifiers) : Bool := + m.visibility.isInferredPublic env def Modifiers.isPartial : Modifiers → Bool | { recKind := .partial, .. } => true @@ -123,8 +137,9 @@ instance : ToFormat Modifiers := ⟨fun m => | none => []) ++ (match m.visibility with | .regular => [] + | .private => [f!"private"] | .protected => [f!"protected"] - | .private => [f!"private"]) + | .public => [f!"public"]) ++ (match m.computeKind with | .regular => [] | .meta => [f!"meta"] | .noncomputable => [f!"noncomputable"]) ++ (match m.recKind with | RecKind.partial => [f!"partial"] | RecKind.nonrec => [f!"nonrec"] | _ => []) ++ (if m.isUnsafe then [f!"unsafe"] else []) @@ -169,12 +184,13 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers : RecKind.nonrec let docString? := docCommentStx.getOptional?.map TSyntax.mk let visibility ← match visibilityStx.getOptional? with - | none => pure Visibility.regular + | none => pure .regular | some v => - let kind := v.getKind - if kind == ``Parser.Command.private then pure Visibility.private - else if kind == ``Parser.Command.protected then pure Visibility.protected - else throwErrorAt v "unexpected visibility modifier" + match v with + | `(Parser.Command.visibility| private) => pure .private + | `(Parser.Command.visibility| protected) => pure .protected + | `(Parser.Command.visibility| public) => pure .public + | _ => throwErrorAt v "unexpected visibility modifier" let attrs ← match attrsStx.getOptional? with | none => pure #[] | some attrs => elabDeclAttrs attrs @@ -189,18 +205,13 @@ If `private`, return the updated name using our internal encoding for private na If `protected`, register `declName` as protected in the environment. -/ def applyVisibility (visibility : Visibility) (declName : Name) : m Name := do - match visibility with - | .private => - let declName := mkPrivateName (← getEnv) declName - checkNotAlreadyDeclared declName - return declName - | .protected => - checkNotAlreadyDeclared declName + let mut declName := declName + if !visibility.isInferredPublic (← getEnv) then + declName := mkPrivateName (← getEnv) declName + checkNotAlreadyDeclared declName + if visibility matches .protected then modifyEnv fun env => addProtected env declName - return declName - | _ => - checkNotAlreadyDeclared declName - pure declName + pure declName def checkIfShadowingStructureField (declName : Name) : m Unit := do match declName with diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index f12b8e7d6a..bce30a2122 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -152,27 +152,25 @@ def expandNamespacedDeclaration : Macro := fun stx => do | none => Macro.throwUnsupported @[builtin_command_elab declaration, builtin_incremental] -def elabDeclaration : CommandElab := fun stx => - -- We assume by default that data from declarations will be exported. Specific elaborators can - -- then nest inside `withoutExporting` for non-exported parts. - withExporting do +def elabDeclaration : CommandElab := fun stx => do + withExporting (isExporting := (← getScope).isPublic) do + let modifiers : TSyntax ``Parser.Command.declModifiers := ⟨stx[0]⟩ let decl := stx[1] let declKind := decl.getKind if isDefLike decl then -- only case implementing incrementality currently elabMutualDef #[stx] else withoutCommandIncrementality true do - let modifiers : TSyntax ``Parser.Command.declModifiers := ⟨stx[0]⟩ - if declKind == ``Lean.Parser.Command.«axiom» then - let modifiers ← elabModifiers modifiers - elabAxiom modifiers decl - else if declKind == ``Lean.Parser.Command.«inductive» - || declKind == ``Lean.Parser.Command.classInductive - || declKind == ``Lean.Parser.Command.«structure» then - let modifiers ← elabModifiers modifiers - elabInductive modifiers decl - else - throwError "unexpected declaration" + let modifiers ← elabModifiers modifiers + withExporting (isExporting := modifiers.isInferredPublic (← getEnv)) do + if declKind == ``Lean.Parser.Command.«axiom» then + elabAxiom modifiers decl + else if declKind == ``Lean.Parser.Command.«inductive» + || declKind == ``Lean.Parser.Command.classInductive + || declKind == ``Lean.Parser.Command.«structure» then + elabInductive modifiers decl + else + throwError "unexpected declaration" /-- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/ private def isMutualDef (stx : Syntax) : Bool := @@ -273,6 +271,7 @@ def expandMutualPreamble : Macro := fun stx => @[builtin_command_elab «mutual», builtin_incremental] def elabMutual : CommandElab := fun stx => do + withExporting (isExporting := (← getScope).isPublic) do if isMutualDef stx then -- only case implementing incrementality currently elabMutualDef stx[1].getArgs diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean index 8369722c42..76c0769f42 100644 --- a/src/Lean/Elab/Import.lean +++ b/src/Lean/Elab/Import.lean @@ -22,10 +22,6 @@ def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Arr | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) => let imports := if preludeTk.isNone && includeInit then #[{ module := `Init : Import }] else #[] imports ++ importsStx.map fun - -- TODO: delete together with `private` keyword - | `(Parser.Module.import| $[private%$privateTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) => - { module := n.getId, importAll := allTk.isSome, isExported := privateTk.isNone - isMeta := metaTk.isSome } | `(Parser.Module.import| $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) => { module := n.getId, importAll := allTk.isSome isExported := publicTk.isSome || moduleTk.isNone diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 962e3d1ef9..796d1de9b8 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -1219,10 +1219,11 @@ where Core.logSnapshotTask { stx? := none, task := (← BaseIO.asTask (act ())), cancelTk? := cancelTk } applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation - finishElab headers (isExporting := false) := withFunLocalDecls headers fun funFVars => + finishElab headers (isExporting := false) := withFunLocalDecls headers fun funFVars => do + let env ← getEnv withExporting (isExporting := !headers.all (fun header => - header.modifiers.isPrivate || header.modifiers.attrs.any (·.name == `no_expose)) && + !header.modifiers.isInferredPublic env || header.modifiers.attrs.any (·.name == `no_expose)) && (isExporting || headers.all (fun header => (header.kind matches .abbrev | .instance)) || (headers.all (·.kind == .def) && sc.attrs.any (· matches `(attrInstance| expose))) || diff --git a/src/Lean/Elab/ParseImportsFast.lean b/src/Lean/Elab/ParseImportsFast.lean index ee07595cce..82f040756f 100644 --- a/src/Lean/Elab/ParseImportsFast.lean +++ b/src/Lean/Elab/ParseImportsFast.lean @@ -195,7 +195,7 @@ def setIsMeta (isMeta : Bool) : Parser := fun _ s => { s with isMeta } def setIsExported (isExported : Bool) : Parser := fun _ s => - { s with isExported } + { s with isExported := isExported || !s.isModule } def setImportAll (importAll : Bool) : Parser := fun _ s => { s with importAll } @@ -203,9 +203,7 @@ def setImportAll (importAll : Bool) : Parser := fun _ s => def main : Parser := keywordCore "module" (fun _ s => s) (fun _ s => { s with isModule := true }) >> keywordCore "prelude" (fun _ s => s.pushImport `Init) (fun _ s => s) >> - many (keywordCore "private" (setIsExported true) (setIsExported false) >> - -- TODO: unset exported when absent and remove `private` - keywordCore "public" (setIsExported true) (setIsExported true) >> + many (keywordCore "public" (setIsExported true) (setIsExported true) >> keywordCore "meta" (setIsMeta false) (setIsMeta true) >> keyword "import" >> keywordCore "all" (setImportAll false) (setImportAll true) >> diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 755abd5399..6ee413dc7e 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -59,7 +59,8 @@ def optNamedPrio := optional namedPrio def «private» := leading_parser "private " def «protected» := leading_parser "protected " -def visibility := «private» <|> «protected» +def «public» := leading_parser "public " +def visibility := «private» <|> «protected» <|> «public» def «meta» := leading_parser "meta " def «noncomputable» := leading_parser "noncomputable " def «unsafe» := leading_parser "unsafe " @@ -69,7 +70,7 @@ def «nonrec» := leading_parser "nonrec " /-- `declModifiers` is the collection of modifiers on a declaration: * a doc comment `/-- ... -/` * a list of attributes `@[attr1, attr2]` -* a visibility specifier, `private` or `protected` +* a visibility specifier, `private`, `protected`, or `public` * `noncomputable` * `unsafe` * `partial` or `nonrec` diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index 8cb722001f..72dc9c05ed 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -13,13 +13,11 @@ namespace Parser namespace Module def moduleTk := leading_parser "module" def «prelude» := leading_parser "prelude" --- TODO: delete -def «private» := leading_parser (withAnonymousAntiquot := false) "private" def «public» := leading_parser (withAnonymousAntiquot := false) "public" def «meta» := leading_parser (withAnonymousAntiquot := false) "meta" def «all» := leading_parser (withAnonymousAntiquot := false) "all" def «import» := leading_parser - atomic (optional («private» <|> «public») >> optional «meta» >> "import ") >> + atomic (optional «public» >> optional «meta» >> "import ") >> optional all >> identWithPartialTrailingDot def header := leading_parser optional (moduleTk >> ppLine >> ppLine) >> diff --git a/src/Lean/Server/Completion/ImportCompletion.lean b/src/Lean/Server/Completion/ImportCompletion.lean index 3984e33cce..0954840c01 100644 --- a/src/Lean/Server/Completion/ImportCompletion.lean +++ b/src/Lean/Server/Completion/ImportCompletion.lean @@ -52,7 +52,7 @@ def computePartialImportCompletions let `(Parser.Module.header| $[module]? $[prelude]? $importsStx*) := headerStx | return #[] let some (completePrefix, incompleteSuffix) := importsStx.findSome? fun importStx => do - let `(Parser.Module.«import»| $[private]? $[meta]? import $[all]? $importId $[.%$trailingDotTk?$_]?) := importStx + let `(Parser.Module.«import»| $[public]? $[meta]? import $[all]? $importId $[.%$trailingDotTk?$_]?) := importStx | unreachable! match trailingDotTk? with | none => diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index c4b7657fd7..f8a27c4480 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -131,7 +131,7 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx) return #[] let locationLinksFromImport (i : Elab.Info) := do - let `(Parser.Module.import| $[private]? $[meta]? import $[all]? $mod) := i.stx + let `(Parser.Module.import| $[public]? $[meta]? import $[all]? $mod) := i.stx | return #[] if let some modUri ← documentUriFromModule? mod.getId then let range := { start := ⟨0, 0⟩, «end» := ⟨0, 0⟩ : Range } diff --git a/tests/pkg/module/Module.lean b/tests/pkg/module/Module.lean index bfbbc7b08e..39ee9f25b5 100644 --- a/tests/pkg/module/Module.lean +++ b/tests/pkg/module/Module.lean @@ -1,11 +1,11 @@ -import Lean -import Module.Basic -import Module.Imported -import Module.ImportedAll -import Module.ImportedPrivateImported -import Module.PrivateImported -import Module.ImportedAllPrivateImported -import Module.NonModule +public import Lean +public import Module.Basic +public import Module.Imported +public import Module.ImportedAll +public import Module.ImportedPrivateImported +public import Module.PrivateImported +public import Module.ImportedAllPrivateImported +public import Module.NonModule /-! # Module system basic tests -/ diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 277f308d65..0b029fb9f6 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -1,17 +1,17 @@ module -axiom testSorry : α +public axiom testSorry : α /-! Module docstring -/ /-- A definition (not exposed). -/ -def f := 1 +public def f := 1 /-- An definition (exposed) -/ -@[expose] def fexp := 1 +@[expose] public def fexp := 1 #guard_msgs(drop warning) in /-- A theorem. -/ -theorem t : f = 1 := testSorry +public theorem t : f = 1 := testSorry -- Check that the theorem types are checked in exported context, where `f` is not defeq to `1` -- (but `fexp` is) @@ -25,11 +25,11 @@ but is expected to have type Vector Unit f : Type -/ #guard_msgs in -theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry +public theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry -private theorem v' (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry +theorem v' (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry -private theorem v'' (x : Vector Unit fexp) (y : Vector Unit 1) : x = y := testSorry +theorem v'' (x : Vector Unit fexp) (y : Vector Unit 1) : x = y := testSorry -- Check that rfl theorems are complained about if they aren't rfl in the context of their type @@ -42,7 +42,7 @@ is not definitionally equal to the right-hand side Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed. -/ #guard_msgs in -theorem trfl : f = 1 := rfl +public theorem trfl : f = 1 := rfl /-- error: Not a definitional equality: the left-hand side f @@ -52,18 +52,18 @@ is not definitionally equal to the right-hand side Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed. -/ #guard_msgs in -@[defeq] theorem trfl' : f = 1 := (rfl) +@[defeq] public theorem trfl' : f = 1 := (rfl) -private theorem trflprivate : f = 1 := rfl -private def trflprivate' : f = 1 := rfl -@[defeq] private def trflprivate''' : f = 1 := rfl -private theorem trflprivate'''' : f = 1 := (rfl) +theorem trflprivate : f = 1 := rfl +def trflprivate' : f = 1 := rfl +@[defeq] def trflprivate''' : f = 1 := rfl +theorem trflprivate'''' : f = 1 := (rfl) -theorem fexp_trfl : fexp = 1 := rfl -@[defeq] theorem fexp_trfl' : fexp = 1 := rfl +public theorem fexp_trfl : fexp = 1 := rfl +@[defeq] public theorem fexp_trfl' : fexp = 1 := rfl -opaque P : Nat → Prop -axiom hP1 : P 1 +public opaque P : Nat → Prop +public axiom hP1 : P 1 /-- error: dsimp made no progress -/ #guard_msgs in @@ -94,30 +94,30 @@ is not definitionally equal to the right-hand side 2 -/ #guard_msgs in -@[defeq] theorem not_rfl : f = 2 := testSorry +@[defeq] public theorem not_rfl : f = 2 := testSorry -private def priv := 2 +def priv := 2 /-! Private decls should not be accessible in exported contexts. -/ /-- error: unknown identifier 'priv' -/ #guard_msgs in -abbrev h := priv +public abbrev h := priv /-! Equational theorems tests. -/ -def f_struct : Nat → Nat +public def f_struct : Nat → Nat | 0 => 0 | n + 1 => f_struct n termination_by structural n => n -def f_wfrec : Nat → Nat → Nat +public def f_wfrec : Nat → Nat → Nat | 0, acc => acc | n + 1, acc => f_wfrec n (acc + 1) termination_by n => n -@[expose] def f_exp_wfrec : Nat → Nat → Nat +@[expose] public def f_exp_wfrec : Nat → Nat → Nat | 0, acc => acc | n + 1, acc => f_exp_wfrec n (acc + 1) termination_by n => n @@ -129,11 +129,11 @@ termination_by n => n /-- error: 'f.eq_def' is a reserved name -/ #guard_msgs in -def f.eq_def := 1 +public def f.eq_def := 1 /-- error: 'fexp.eq_def' is a reserved name -/ #guard_msgs in -def fexp.eq_def := 1 +public def fexp.eq_def := 1 /-- info: @[defeq] private theorem f.eq_def : f = 1 -/ #guard_msgs in #print sig f.eq_def diff --git a/tests/pkg/module/Module/Imported.lean b/tests/pkg/module/Module/Imported.lean index f3352b3996..58bf4d715b 100644 --- a/tests/pkg/module/Module/Imported.lean +++ b/tests/pkg/module/Module/Imported.lean @@ -1,7 +1,7 @@ module prelude -import Module.Basic +public import Module.Basic /-! Definitions should be exported without their bodies by default -/ diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index 41c06bae6c..1b76c403fd 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/tests/pkg/module/Module/ImportedAll.lean @@ -1,7 +1,7 @@ module prelude -import all Module.Basic +public import all Module.Basic /-! `import all` should import private information, privately. -/ @@ -21,7 +21,7 @@ but is expected to have type Vector Unit f : Type -/ #guard_msgs in -theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := sorry +public theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := sorry /-- error: dsimp made no progress -/ #guard_msgs in @@ -127,8 +127,8 @@ info: theorem f_exp_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat /-! `import all` should allow access to private defs, privately. -/ -def pub := priv +public def pub := priv /-- error: unknown identifier 'priv' -/ #guard_msgs in -@[expose] def pub' := priv +@[expose] public def pub' := priv diff --git a/tests/pkg/module/Module/ImportedAllPrivateImported.lean b/tests/pkg/module/Module/ImportedAllPrivateImported.lean index 34960b6afa..e71e2fb8b2 100644 --- a/tests/pkg/module/Module/ImportedAllPrivateImported.lean +++ b/tests/pkg/module/Module/ImportedAllPrivateImported.lean @@ -1,7 +1,7 @@ module prelude -import all Module.PrivateImported +public import all Module.PrivateImported /-! `import all` should activate nested `private import`s. -/ diff --git a/tests/pkg/module/Module/ImportedImportedAll.lean b/tests/pkg/module/Module/ImportedImportedAll.lean index 6a7da3d15b..b306ebfbf2 100644 --- a/tests/pkg/module/Module/ImportedImportedAll.lean +++ b/tests/pkg/module/Module/ImportedImportedAll.lean @@ -1,7 +1,7 @@ module prelude -import Module.ImportedAll +public import Module.ImportedAll /-! `import all` should not transitively expose private info. -/ diff --git a/tests/pkg/module/Module/ImportedPrivateImported.lean b/tests/pkg/module/Module/ImportedPrivateImported.lean index a11e0bddff..00d3a32bfb 100644 --- a/tests/pkg/module/Module/ImportedPrivateImported.lean +++ b/tests/pkg/module/Module/ImportedPrivateImported.lean @@ -1,7 +1,7 @@ module prelude -import Module.PrivateImported +public import Module.PrivateImported /-! `private import` should not be transitive. -/ diff --git a/tests/pkg/module/Module/NonModule.lean b/tests/pkg/module/Module/NonModule.lean index 48bfa62e2b..8d594390c0 100644 --- a/tests/pkg/module/Module/NonModule.lean +++ b/tests/pkg/module/Module/NonModule.lean @@ -1,5 +1,5 @@ -import Module.Basic -import Lean +public import Module.Basic +public import Lean /-- info: @[defeq] theorem f.eq_def : f = 1 -/ #guard_msgs in #print sig f.eq_def diff --git a/tests/pkg/module/Module/PrivateImported.lean b/tests/pkg/module/Module/PrivateImported.lean index e9a9cc791d..e872bb02b1 100644 --- a/tests/pkg/module/Module/PrivateImported.lean +++ b/tests/pkg/module/Module/PrivateImported.lean @@ -1,16 +1,16 @@ module -private import Module.Basic +import Module.Basic /-! `private import` should allow only private access to imported decls. -/ -def g := f +public def g := f /-- error: unknown identifier 'f' -/ #guard_msgs in set_option autoImplicit false in -theorem t2 : f = 1 := sorry +public theorem t2 : f = 1 := sorry /-- error: unknown identifier 'f' -/ #guard_msgs in -@[expose] def h : True := f +@[expose] public def h : True := f