From 232a0495b0b11e6817adfed89b1e913bbbc34157 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 6 Oct 2025 15:30:48 +0200 Subject: [PATCH] chore: remove `public section` from end of files (#10684) This PR removes `public section` lines from end of files; they look a bit silly there. --- src/Init/Control.lean | 2 -- src/Init/Control/Lawful.lean | 2 -- src/Init/Control/Lawful/MonadLift.lean | 2 -- src/Init/Data.lean | 2 -- src/Init/Data/Array.lean | 2 -- src/Init/Data/Array/Lex.lean | 2 -- src/Init/Data/Array/QSort.lean | 2 -- src/Init/Data/Basic.lean | 2 -- src/Init/Data/BitVec.lean | 2 -- src/Init/Data/ByteArray.lean | 2 -- src/Init/Data/Char.lean | 2 -- src/Init/Data/Fin.lean | 2 -- src/Init/Data/FloatArray.lean | 2 -- src/Init/Data/Format.lean | 2 -- src/Init/Data/Int.lean | 2 -- src/Init/Data/Int/Bitwise.lean | 2 -- src/Init/Data/Int/DivMod.lean | 2 -- src/Init/Data/Iterators/Combinators.lean | 2 -- src/Init/Data/Iterators/Combinators/Monadic.lean | 2 -- src/Init/Data/Iterators/Consumers.lean | 2 -- src/Init/Data/Iterators/Consumers/Monadic.lean | 2 -- src/Init/Data/Iterators/Internal.lean | 2 -- src/Init/Data/Iterators/Lemmas.lean | 2 -- src/Init/Data/Iterators/Lemmas/Combinators.lean | 2 -- src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean | 2 -- src/Init/Data/Iterators/Lemmas/Consumers.lean | 2 -- src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean | 2 -- src/Init/Data/List.lean | 2 -- src/Init/Data/List/Nat.lean | 2 -- src/Init/Data/List/Sort.lean | 2 -- src/Init/Data/Nat.lean | 2 -- src/Init/Data/Nat/Bitwise.lean | 2 -- src/Init/Data/Nat/Div.lean | 2 -- src/Init/Data/Option.lean | 2 -- src/Init/Data/Range.lean | 2 -- src/Init/Data/Slice/Array.lean | 2 -- src/Init/Data/String.lean | 2 -- src/Init/Data/Sum.lean | 2 -- src/Init/Data/ToString.lean | 2 -- src/Init/Data/UInt.lean | 2 -- src/Init/Data/Vector.lean | 2 -- src/Init/Grind/Module.lean | 1 - src/Init/Grind/Ordered.lean | 2 -- src/Init/GrindInstances.lean | 2 -- src/Init/GrindInstances/Ring.lean | 2 -- src/Init/Internal/Order.lean | 2 -- src/Init/Omega.lean | 2 -- src/Init/System.lean | 2 -- src/Lean/Compiler.lean | 2 -- src/Lean/Compiler/LCNF.lean | 2 -- src/Lean/Data.lean | 2 -- src/Lean/Data/Json.lean | 2 -- src/Lean/Data/Json/FromToJson.lean | 2 -- src/Lean/Data/Lsp.lean | 2 -- src/Lean/Data/Xml.lean | 2 -- src/Lean/Elab.lean | 2 -- src/Lean/Elab/InfoTree.lean | 2 -- src/Lean/Elab/PreDefinition.lean | 2 -- src/Lean/Elab/PreDefinition/PartialFixpoint.lean | 2 -- src/Lean/Elab/PreDefinition/Structural.lean | 2 -- src/Lean/Elab/PreDefinition/WF.lean | 2 -- src/Lean/Elab/Tactic.lean | 2 -- src/Lean/Elab/Tactic/Conv.lean | 2 -- src/Lean/Elab/Tactic/Do.lean | 2 -- src/Lean/Elab/Tactic/Do/ProofMode.lean | 2 -- src/Lean/ErrorExplanations.lean | 2 -- src/Lean/Linter.lean | 2 -- src/Lean/Meta/Constructions.lean | 2 -- src/Lean/Meta/Match/MatcherApp.lean | 2 -- src/Lean/Meta/Tactic.lean | 2 -- src/Lean/Meta/Tactic/AC.lean | 2 -- src/Lean/Meta/Tactic/Grind/Arith.lean | 1 - src/Lean/Meta/Tactic/Grind/Arith/Model.lean | 2 -- src/Lean/Meta/Tactic/Simp/Arith/Int.lean | 2 -- src/Lean/Meta/Tactic/Simp/Arith/Nat.lean | 2 -- src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean | 2 -- src/Lean/PrettyPrinter/Delaborator.lean | 2 -- src/Lean/Server.lean | 2 -- src/Lean/Server/CodeActions.lean | 2 -- src/Lean/Server/Rpc.lean | 2 -- src/Lean/Server/Test.lean | 2 -- src/Lean/Util.lean | 2 -- src/Lean/Widget.lean | 2 -- src/Std/Data.lean | 2 -- src/Std/Data/DHashMap.lean | 2 -- src/Std/Data/DTreeMap.lean | 2 -- src/Std/Data/DTreeMap/Raw.lean | 2 -- src/Std/Data/ExtDHashMap.lean | 2 -- src/Std/Data/ExtDTreeMap.lean | 2 -- src/Std/Data/ExtHashMap.lean | 2 -- src/Std/Data/ExtHashSet.lean | 2 -- src/Std/Data/ExtTreeMap.lean | 2 -- src/Std/Data/ExtTreeSet.lean | 2 -- src/Std/Data/HashMap.lean | 2 -- src/Std/Data/HashSet.lean | 2 -- src/Std/Data/Iterators/Combinators.lean | 2 -- src/Std/Data/Iterators/Combinators/Monadic.lean | 2 -- src/Std/Data/Iterators/Lemmas.lean | 2 -- src/Std/Data/Iterators/Lemmas/Combinators.lean | 2 -- src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean | 2 -- src/Std/Data/Iterators/Lemmas/Consumers.lean | 2 -- src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean | 2 -- src/Std/Data/Iterators/Lemmas/Equivalence.lean | 2 -- src/Std/Data/Iterators/Lemmas/Monadic.lean | 2 -- src/Std/Data/Iterators/Lemmas/Producers.lean | 2 -- src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean | 2 -- src/Std/Data/Iterators/Producers.lean | 2 -- src/Std/Data/Iterators/Producers/Monadic.lean | 2 -- src/Std/Data/TreeMap.lean | 2 -- src/Std/Data/TreeMap/Raw.lean | 2 -- src/Std/Data/TreeSet.lean | 2 -- src/Std/Data/TreeSet/Raw.lean | 2 -- src/Std/Do.lean | 2 -- src/Std/Do/SPred.lean | 2 -- src/Std/Do/Triple.lean | 2 -- src/Std/Do/WP.lean | 2 -- src/Std/Internal/Async.lean | 2 -- src/Std/Internal/Parsec.lean | 2 -- src/Std/Internal/UV.lean | 2 -- src/Std/Net.lean | 2 -- src/Std/Sat.lean | 2 -- src/Std/Sat/AIG.lean | 2 -- src/Std/Sat/AIG/RefVecOperator.lean | 2 -- src/Std/Sat/CNF.lean | 2 -- src/Std/Sync.lean | 2 -- src/Std/Time/Date.lean | 2 -- src/Std/Time/Internal.lean | 2 -- src/Std/Time/Time.lean | 2 -- src/Std/Time/Time/Basic.lean | 2 -- 129 files changed, 256 deletions(-) diff --git a/src/Init/Control.lean b/src/Init/Control.lean index 3e06fc820e..d0f8b5c088 100644 --- a/src/Init/Control.lean +++ b/src/Init/Control.lean @@ -16,5 +16,3 @@ 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/Lawful.lean b/src/Init/Control/Lawful.lean index 1f2fe2c06a..d9d1703c8a 100644 --- a/src/Init/Control/Lawful.lean +++ b/src/Init/Control/Lawful.lean @@ -10,5 +10,3 @@ 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/MonadLift.lean b/src/Init/Control/Lawful/MonadLift.lean index 42811f6638..7bde8699e2 100644 --- a/src/Init/Control/Lawful/MonadLift.lean +++ b/src/Init/Control/Lawful/MonadLift.lean @@ -9,5 +9,3 @@ prelude 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/Data.lean b/src/Init/Data.lean index d408770268..27a79eb777 100644 --- a/src/Init/Data.lean +++ b/src/Init/Data.lean @@ -53,5 +53,3 @@ public import Init.Data.Slice public import Init.Data.Order public import Init.Data.Rat public import Init.Data.Dyadic - -public section diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean index 0afae8e992..5262c7fcb2 100644 --- a/src/Init/Data/Array.lean +++ b/src/Init/Data/Array.lean @@ -30,5 +30,3 @@ 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/Lex.lean b/src/Init/Data/Array/Lex.lean index ce0a5f7f8d..f2205d170a 100644 --- a/src/Init/Data/Array/Lex.lean +++ b/src/Init/Data/Array/Lex.lean @@ -8,5 +8,3 @@ module prelude public import Init.Data.Array.Lex.Basic public import Init.Data.Array.Lex.Lemmas - -public section diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean index 8919cb66ca..4d65058a77 100644 --- a/src/Init/Data/Array/QSort.lean +++ b/src/Init/Data/Array/QSort.lean @@ -7,5 +7,3 @@ module prelude public import Init.Data.Array.QSort.Basic - -public section diff --git a/src/Init/Data/Basic.lean b/src/Init/Data/Basic.lean index 418cf55401..93b9d3f0d4 100644 --- a/src/Init/Data/Basic.lean +++ b/src/Init/Data/Basic.lean @@ -16,5 +16,3 @@ 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 35d77c06f6..6616f4ffe6 100644 --- a/src/Init/Data/BitVec.lean +++ b/src/Init/Data/BitVec.lean @@ -13,5 +13,3 @@ 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/ByteArray.lean b/src/Init/Data/ByteArray.lean index a9a32612cd..eeab7dd85f 100644 --- a/src/Init/Data/ByteArray.lean +++ b/src/Init/Data/ByteArray.lean @@ -10,5 +10,3 @@ public import Init.Data.ByteArray.Basic public import Init.Data.ByteArray.Bootstrap public import Init.Data.ByteArray.Extra public import Init.Data.ByteArray.Lemmas - -public section diff --git a/src/Init/Data/Char.lean b/src/Init/Data/Char.lean index 1dc5be75bd..d920537fe8 100644 --- a/src/Init/Data/Char.lean +++ b/src/Init/Data/Char.lean @@ -9,5 +9,3 @@ prelude public import Init.Data.Char.Basic public import Init.Data.Char.Lemmas public import Init.Data.Char.Order - -public section diff --git a/src/Init/Data/Fin.lean b/src/Init/Data/Fin.lean index 014a77e9ab..18cce10f8d 100644 --- a/src/Init/Data/Fin.lean +++ b/src/Init/Data/Fin.lean @@ -11,5 +11,3 @@ 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/FloatArray.lean b/src/Init/Data/FloatArray.lean index 4dd9bd0808..6290de4536 100644 --- a/src/Init/Data/FloatArray.lean +++ b/src/Init/Data/FloatArray.lean @@ -7,5 +7,3 @@ module prelude public import Init.Data.FloatArray.Basic - -public section diff --git a/src/Init/Data/Format.lean b/src/Init/Data/Format.lean index 6537fd89a6..66a542adf1 100644 --- a/src/Init/Data/Format.lean +++ b/src/Init/Data/Format.lean @@ -10,5 +10,3 @@ 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/Int.lean b/src/Init/Data/Int.lean index eb4d426b70..bf417b09a9 100644 --- a/src/Init/Data/Int.lean +++ b/src/Init/Data/Int.lean @@ -18,5 +18,3 @@ 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/Bitwise.lean b/src/Init/Data/Int/Bitwise.lean index 8b0506ceca..71bd962533 100644 --- a/src/Init/Data/Int/Bitwise.lean +++ b/src/Init/Data/Int/Bitwise.lean @@ -8,5 +8,3 @@ module prelude public import Init.Data.Int.Bitwise.Basic public import Init.Data.Int.Bitwise.Lemmas - -public section diff --git a/src/Init/Data/Int/DivMod.lean b/src/Init/Data/Int/DivMod.lean index cf883cf170..58702906f3 100644 --- a/src/Init/Data/Int/DivMod.lean +++ b/src/Init/Data/Int/DivMod.lean @@ -9,5 +9,3 @@ prelude 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/Iterators/Combinators.lean b/src/Init/Data/Iterators/Combinators.lean index c48bdaa250..3081e2e81e 100644 --- a/src/Init/Data/Iterators/Combinators.lean +++ b/src/Init/Data/Iterators/Combinators.lean @@ -9,5 +9,3 @@ prelude 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/Monadic.lean b/src/Init/Data/Iterators/Combinators/Monadic.lean index e02c2d097f..0b908ab537 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic.lean @@ -8,5 +8,3 @@ module prelude 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/Consumers.lean b/src/Init/Data/Iterators/Consumers.lean index e04ead2e4a..4b9e068574 100644 --- a/src/Init/Data/Iterators/Consumers.lean +++ b/src/Init/Data/Iterators/Consumers.lean @@ -13,5 +13,3 @@ public import Init.Data.Iterators.Consumers.Loop public import Init.Data.Iterators.Consumers.Partial public import Init.Data.Iterators.Consumers.Stream - -public section diff --git a/src/Init/Data/Iterators/Consumers/Monadic.lean b/src/Init/Data/Iterators/Consumers/Monadic.lean index c8bec732b5..0e3b43e067 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic.lean @@ -10,5 +10,3 @@ 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/Internal.lean b/src/Init/Data/Iterators/Internal.lean index 8dfbaf3501..6b1ca2926e 100644 --- a/src/Init/Data/Iterators/Internal.lean +++ b/src/Init/Data/Iterators/Internal.lean @@ -8,5 +8,3 @@ module prelude public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction public import Init.Data.Iterators.Internal.Termination - -public section diff --git a/src/Init/Data/Iterators/Lemmas.lean b/src/Init/Data/Iterators/Lemmas.lean index ad0af047a5..a37692c19f 100644 --- a/src/Init/Data/Iterators/Lemmas.lean +++ b/src/Init/Data/Iterators/Lemmas.lean @@ -8,5 +8,3 @@ module prelude public import Init.Data.Iterators.Lemmas.Consumers public import Init.Data.Iterators.Lemmas.Combinators - -public section diff --git a/src/Init/Data/Iterators/Lemmas/Combinators.lean b/src/Init/Data/Iterators/Lemmas/Combinators.lean index e57ea267ac..c7671bc49f 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators.lean @@ -10,5 +10,3 @@ 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/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean index d707eec87a..9821eb5856 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean @@ -9,5 +9,3 @@ prelude 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/Consumers.lean b/src/Init/Data/Iterators/Lemmas/Consumers.lean index b6cae0c957..914bc73b87 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers.lean @@ -9,5 +9,3 @@ prelude 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/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean index 5e60a3b4fb..590aa8908d 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean @@ -8,5 +8,3 @@ module prelude 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/List.lean b/src/Init/Data/List.lean index 59bbe26951..cd174f3620 100644 --- a/src/Init/Data/List.lean +++ b/src/Init/Data/List.lean @@ -31,5 +31,3 @@ 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/Nat.lean b/src/Init/Data/List/Nat.lean index fcaad2266c..ea64626eae 100644 --- a/src/Init/Data/List/Nat.lean +++ b/src/Init/Data/List/Nat.lean @@ -18,5 +18,3 @@ 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/Sort.lean b/src/Init/Data/List/Sort.lean index 292dd5d2a8..6f100a03f6 100644 --- a/src/Init/Data/List/Sort.lean +++ b/src/Init/Data/List/Sort.lean @@ -9,5 +9,3 @@ prelude 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/Nat.lean b/src/Init/Data/Nat.lean index da552874b1..ce79f348a5 100644 --- a/src/Init/Data/Nat.lean +++ b/src/Init/Data/Nat.lean @@ -26,5 +26,3 @@ public import Init.Data.Nat.Compare public import Init.Data.Nat.Simproc public import Init.Data.Nat.Fold public import Init.Data.Nat.Order - -public section diff --git a/src/Init/Data/Nat/Bitwise.lean b/src/Init/Data/Nat/Bitwise.lean index a25b26edc8..e147cbc517 100644 --- a/src/Init/Data/Nat/Bitwise.lean +++ b/src/Init/Data/Nat/Bitwise.lean @@ -8,5 +8,3 @@ module prelude public import Init.Data.Nat.Bitwise.Basic public import Init.Data.Nat.Bitwise.Lemmas - -public section diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index d041f146a9..1c6e021786 100644 --- a/src/Init/Data/Nat/Div.lean +++ b/src/Init/Data/Nat/Div.lean @@ -8,5 +8,3 @@ module prelude public import Init.Data.Nat.Div.Basic public import Init.Data.Nat.Div.Lemmas - -public section diff --git a/src/Init/Data/Option.lean b/src/Init/Data/Option.lean index a025a89f98..ea1f54855e 100644 --- a/src/Init/Data/Option.lean +++ b/src/Init/Data/Option.lean @@ -15,5 +15,3 @@ 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/Range.lean b/src/Init/Data/Range.lean index ebf0732d69..55e2901584 100644 --- a/src/Init/Data/Range.lean +++ b/src/Init/Data/Range.lean @@ -8,5 +8,3 @@ module prelude public import Init.Data.Range.Basic public import Init.Data.Range.Lemmas - -public section diff --git a/src/Init/Data/Slice/Array.lean b/src/Init/Data/Slice/Array.lean index a6f259ffb3..06d3020b1c 100644 --- a/src/Init/Data/Slice/Array.lean +++ b/src/Init/Data/Slice/Array.lean @@ -9,5 +9,3 @@ prelude 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/String.lean b/src/Init/Data/String.lean index d67db3fc2e..3fccca09b3 100644 --- a/src/Init/Data/String.lean +++ b/src/Init/Data/String.lean @@ -16,5 +16,3 @@ public import Init.Data.String.Bootstrap public import Init.Data.String.Slice public import Init.Data.String.Pattern public import Init.Data.String.Stream - -public section diff --git a/src/Init/Data/Sum.lean b/src/Init/Data/Sum.lean index 2f6af705e5..6d89f77fba 100644 --- a/src/Init/Data/Sum.lean +++ b/src/Init/Data/Sum.lean @@ -8,5 +8,3 @@ module prelude public import Init.Data.Sum.Basic public import Init.Data.Sum.Lemmas - -public section diff --git a/src/Init/Data/ToString.lean b/src/Init/Data/ToString.lean index ffc5186a2d..3a438eb8e7 100644 --- a/src/Init/Data/ToString.lean +++ b/src/Init/Data/ToString.lean @@ -9,5 +9,3 @@ prelude public import Init.Data.ToString.Basic public import Init.Data.ToString.Macro public meta import Init.Data.ToString.Name - -public section diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean index 0d74665bab..30404ef347 100644 --- a/src/Init/Data/UInt.lean +++ b/src/Init/Data/UInt.lean @@ -11,5 +11,3 @@ 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/Vector.lean b/src/Init/Data/Vector.lean index dd6aa8b10b..1a987695bb 100644 --- a/src/Init/Data/Vector.lean +++ b/src/Init/Data/Vector.lean @@ -24,5 +24,3 @@ public import Init.Data.Vector.Perm public import Init.Data.Vector.Find public import Init.Data.Vector.Algebra public import Init.Data.Vector.Stream - -public section diff --git a/src/Init/Grind/Module.lean b/src/Init/Grind/Module.lean index ea282eb333..ea1738f8b3 100644 --- a/src/Init/Grind/Module.lean +++ b/src/Init/Grind/Module.lean @@ -9,4 +9,3 @@ public import Init.Grind.Module.Basic public import Init.Grind.Module.Envelope public import Init.Grind.Module.OfNatModule public import Init.Grind.Module.NatModuleNorm -public section diff --git a/src/Init/Grind/Ordered.lean b/src/Init/Grind/Ordered.lean index 73cd4d10de..8e8a473338 100644 --- a/src/Init/Grind/Ordered.lean +++ b/src/Init/Grind/Ordered.lean @@ -13,5 +13,3 @@ public import Init.Grind.Ordered.Field public import Init.Grind.Ordered.Int public import Init.Grind.Ordered.Rat public import Init.Grind.Ordered.Linarith - -public section diff --git a/src/Init/GrindInstances.lean b/src/Init/GrindInstances.lean index 81aba4ad54..08ce1a4bcc 100644 --- a/src/Init/GrindInstances.lean +++ b/src/Init/GrindInstances.lean @@ -9,5 +9,3 @@ prelude public import Init.GrindInstances.ToInt public import Init.GrindInstances.Ring public import Init.GrindInstances.Nat - -public section diff --git a/src/Init/GrindInstances/Ring.lean b/src/Init/GrindInstances/Ring.lean index 5509332f34..4c56577dcb 100644 --- a/src/Init/GrindInstances/Ring.lean +++ b/src/Init/GrindInstances/Ring.lean @@ -13,5 +13,3 @@ public import Init.GrindInstances.Ring.SInt public import Init.GrindInstances.Ring.Fin public import Init.GrindInstances.Ring.BitVec public import Init.GrindInstances.Ring.Rat - -public section diff --git a/src/Init/Internal/Order.lean b/src/Init/Internal/Order.lean index d14bfd6884..7636d75b25 100644 --- a/src/Init/Internal/Order.lean +++ b/src/Init/Internal/Order.lean @@ -9,5 +9,3 @@ prelude 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/Omega.lean b/src/Init/Omega.lean index d39790a10c..a84afe1f73 100644 --- a/src/Init/Omega.lean +++ b/src/Init/Omega.lean @@ -11,5 +11,3 @@ 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/System.lean b/src/Init/System.lean index 2306a4c740..f1bf8963c0 100644 --- a/src/Init/System.lean +++ b/src/Init/System.lean @@ -10,5 +10,3 @@ public import Init.System.IO public import Init.System.Platform public import Init.System.Uri public import Init.System.Promise - -public section diff --git a/src/Lean/Compiler.lean b/src/Lean/Compiler.lean index c655df7011..570c698042 100644 --- a/src/Lean/Compiler.lean +++ b/src/Lean/Compiler.lean @@ -19,5 +19,3 @@ public import Lean.Compiler.MetaAttr public import Lean.Compiler.NoncomputableAttr public import Lean.Compiler.Main public import Lean.Compiler.Old -- TODO: delete after we port code generator to Lean - -public section diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean index bbd62ced6d..204a0495ac 100644 --- a/src/Lean/Compiler/LCNF.lean +++ b/src/Lean/Compiler/LCNF.lean @@ -44,5 +44,3 @@ public import Lean.Compiler.LCNF.Closure public import Lean.Compiler.LCNF.LambdaLifting public import Lean.Compiler.LCNF.ReduceArity public import Lean.Compiler.LCNF.Probing - -public section diff --git a/src/Lean/Data.lean b/src/Lean/Data.lean index 4174bbf568..543f9e699c 100644 --- a/src/Lean/Data.lean +++ b/src/Lean/Data.lean @@ -30,5 +30,3 @@ public import Lean.Data.NameTrie public import Lean.Data.RBTree public import Lean.Data.RBMap public import Lean.Data.RArray - -public section diff --git a/src/Lean/Data/Json.lean b/src/Lean/Data/Json.lean index 88fbd09f1a..04a9c370c5 100644 --- a/src/Lean/Data/Json.lean +++ b/src/Lean/Data/Json.lean @@ -12,5 +12,3 @@ public import Lean.Data.Json.Printer public import Lean.Data.Json.Parser public import Lean.Data.Json.FromToJson public import Lean.Data.Json.Elab - -public section diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index 944580bd20..c2ed935d36 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -9,5 +9,3 @@ module prelude public import Lean.Data.Json.FromToJson.Basic public import Lean.Data.Json.FromToJson.Extra - -public section diff --git a/src/Lean/Data/Lsp.lean b/src/Lean/Data/Lsp.lean index dfd0d5b09b..2c5ae25132 100644 --- a/src/Lean/Data/Lsp.lean +++ b/src/Lean/Data/Lsp.lean @@ -23,5 +23,3 @@ public import Lean.Data.Lsp.Workspace public import Lean.Data.Lsp.Ipc public import Lean.Data.Lsp.CodeActions public import Lean.Data.Lsp.Window - -public section diff --git a/src/Lean/Data/Xml.lean b/src/Lean/Data/Xml.lean index bf67c09098..e0d1808bba 100644 --- a/src/Lean/Data/Xml.lean +++ b/src/Lean/Data/Xml.lean @@ -8,5 +8,3 @@ module prelude public import Lean.Data.Xml.Basic public import Lean.Data.Xml.Parser - -public section diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean index b99ffa35f8..0b597382f6 100644 --- a/src/Lean/Elab.lean +++ b/src/Lean/Elab.lean @@ -62,5 +62,3 @@ public import Lean.Elab.InfoTrees public import Lean.Elab.ErrorExplanation public import Lean.Elab.DocString public import Lean.Elab.DocString.Builtin - -public section diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index 4f501419f5..2bd30aea83 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -9,5 +9,3 @@ module prelude public import Lean.Elab.InfoTree.Types public import Lean.Elab.InfoTree.Main - -public section diff --git a/src/Lean/Elab/PreDefinition.lean b/src/Lean/Elab/PreDefinition.lean index b19147401d..1a05017bc9 100644 --- a/src/Lean/Elab/PreDefinition.lean +++ b/src/Lean/Elab/PreDefinition.lean @@ -14,5 +14,3 @@ public import Lean.Elab.PreDefinition.WF public import Lean.Elab.PreDefinition.Eqns public import Lean.Elab.PreDefinition.Nonrec.Eqns public import Lean.Elab.PreDefinition.EqUnfold - -public section diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint.lean index b10e7d0bbe..262854a4c8 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint.lean @@ -9,5 +9,3 @@ prelude public import Lean.Elab.PreDefinition.PartialFixpoint.Eqns public import Lean.Elab.PreDefinition.PartialFixpoint.Main public import Lean.Elab.PreDefinition.PartialFixpoint.Induction - -public section diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean index 0307c53dc5..40dfc62c11 100644 --- a/src/Lean/Elab/PreDefinition/Structural.lean +++ b/src/Lean/Elab/PreDefinition/Structural.lean @@ -7,5 +7,3 @@ module prelude public import Lean.Elab.PreDefinition.Structural.Main - -public section diff --git a/src/Lean/Elab/PreDefinition/WF.lean b/src/Lean/Elab/PreDefinition/WF.lean index 14bed9e3cc..5d14df3acf 100644 --- a/src/Lean/Elab/PreDefinition/WF.lean +++ b/src/Lean/Elab/PreDefinition/WF.lean @@ -8,5 +8,3 @@ module prelude public import Lean.Elab.PreDefinition.WF.Main public import Lean.Elab.PreDefinition.WF.Eqns - -public section diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 7da838c684..4bcb708a8f 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -55,5 +55,3 @@ public import Lean.Elab.Tactic.SimpArith public import Lean.Elab.Tactic.Show public import Lean.Elab.Tactic.Lets public import Lean.Elab.Tactic.Do - -public section diff --git a/src/Lean/Elab/Tactic/Conv.lean b/src/Lean/Elab/Tactic/Conv.lean index fdf96e4de9..382ee8bec7 100644 --- a/src/Lean/Elab/Tactic/Conv.lean +++ b/src/Lean/Elab/Tactic/Conv.lean @@ -15,5 +15,3 @@ public import Lean.Elab.Tactic.Conv.Simp public import Lean.Elab.Tactic.Conv.Pattern public import Lean.Elab.Tactic.Conv.Delta public import Lean.Elab.Tactic.Conv.Unfold - -public section diff --git a/src/Lean/Elab/Tactic/Do.lean b/src/Lean/Elab/Tactic/Do.lean index d3d595402d..47359990ff 100644 --- a/src/Lean/Elab/Tactic/Do.lean +++ b/src/Lean/Elab/Tactic/Do.lean @@ -12,5 +12,3 @@ public import Lean.Elab.Tactic.Do.Attr public import Lean.Elab.Tactic.Do.LetElim public import Lean.Elab.Tactic.Do.Spec public import Lean.Elab.Tactic.Do.VCGen - -public section diff --git a/src/Lean/Elab/Tactic/Do/ProofMode.lean b/src/Lean/Elab/Tactic/Do/ProofMode.lean index 7ce5f4a05f..a729fd3664 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode.lean @@ -24,5 +24,3 @@ public import Lean.Elab.Tactic.Do.ProofMode.Cases public import Lean.Elab.Tactic.Do.ProofMode.Exfalso public import Lean.Elab.Tactic.Do.ProofMode.Have public import Lean.Elab.Tactic.Do.ProofMode.Refine - -public section diff --git a/src/Lean/ErrorExplanations.lean b/src/Lean/ErrorExplanations.lean index 2f3372f6e6..5fa5f56c6f 100644 --- a/src/Lean/ErrorExplanations.lean +++ b/src/Lean/ErrorExplanations.lean @@ -17,5 +17,3 @@ public import Lean.ErrorExplanations.ProjNonPropFromProp public import Lean.ErrorExplanations.PropRecLargeElim public import Lean.ErrorExplanations.RedundantMatchAlt public import Lean.ErrorExplanations.UnknownIdentifier - -public section diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean index 8107dec49c..4ae5c16450 100644 --- a/src/Lean/Linter.lean +++ b/src/Lean/Linter.lean @@ -17,5 +17,3 @@ public import Lean.Linter.Omit public import Lean.Linter.List public import Lean.Linter.Sets public import Lean.Linter.UnusedSimpArgs - -public section diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean index 7eada680c1..fd020d7f1f 100644 --- a/src/Lean/Meta/Constructions.lean +++ b/src/Lean/Meta/Constructions.lean @@ -11,5 +11,3 @@ public import Lean.Meta.Constructions.NoConfusion public import Lean.Meta.Constructions.RecOn public import Lean.Meta.Constructions.BRecOn public import Lean.Meta.Constructions.CasesOnSameCtor - -public section diff --git a/src/Lean/Meta/Match/MatcherApp.lean b/src/Lean/Meta/Match/MatcherApp.lean index bf87b88537..4dbd8e3c56 100644 --- a/src/Lean/Meta/Match/MatcherApp.lean +++ b/src/Lean/Meta/Match/MatcherApp.lean @@ -8,5 +8,3 @@ module prelude public import Lean.Meta.Match.MatcherApp.Basic public import Lean.Meta.Match.MatcherApp.Transform - -public section diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean index 99b6d289f6..4f7436cdba 100644 --- a/src/Lean/Meta/Tactic.lean +++ b/src/Lean/Meta/Tactic.lean @@ -45,5 +45,3 @@ public import Lean.Meta.Tactic.Rewrites public import Lean.Meta.Tactic.Grind public import Lean.Meta.Tactic.Ext public import Lean.Meta.Tactic.Try - -public section diff --git a/src/Lean/Meta/Tactic/AC.lean b/src/Lean/Meta/Tactic/AC.lean index 73bd1eb66d..37d31f4a61 100644 --- a/src/Lean/Meta/Tactic/AC.lean +++ b/src/Lean/Meta/Tactic/AC.lean @@ -7,5 +7,3 @@ module prelude public import Lean.Meta.Tactic.AC.Main - -public section diff --git a/src/Lean/Meta/Tactic/Grind/Arith.lean b/src/Lean/Meta/Tactic/Grind/Arith.lean index 33bbed807e..d4d4f3314f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith.lean @@ -13,4 +13,3 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing public import Lean.Meta.Tactic.Grind.Arith.Linear public import Lean.Meta.Tactic.Grind.Arith.Cutsat public import Lean.Meta.Tactic.Grind.Arith.Simproc -public section diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Model.lean b/src/Lean/Meta/Tactic/Grind/Arith/Model.lean index f223938b57..6ed823c36f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Model.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Model.lean @@ -8,5 +8,3 @@ module prelude public import Lean.Meta.Tactic.Grind.Arith.Offset.Model public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model - -public section diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Int.lean b/src/Lean/Meta/Tactic/Simp/Arith/Int.lean index 32cfa8fabb..7bf9824343 100644 --- a/src/Lean/Meta/Tactic/Simp/Arith/Int.lean +++ b/src/Lean/Meta/Tactic/Simp/Arith/Int.lean @@ -8,5 +8,3 @@ module prelude public import Lean.Meta.Tactic.Simp.Arith.Int.Basic public import Lean.Meta.Tactic.Simp.Arith.Int.Simp - -public section diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Nat.lean b/src/Lean/Meta/Tactic/Simp/Arith/Nat.lean index 2e4c1e5a02..fd88beae86 100644 --- a/src/Lean/Meta/Tactic/Simp/Arith/Nat.lean +++ b/src/Lean/Meta/Tactic/Simp/Arith/Nat.lean @@ -8,5 +8,3 @@ module prelude public import Lean.Meta.Tactic.Simp.Arith.Nat.Basic public import Lean.Meta.Tactic.Simp.Arith.Nat.Simp - -public section diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean index f333212d11..2b9ae52caa 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean @@ -19,5 +19,3 @@ public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.MethodSpecs public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.CtorIdx - -public section diff --git a/src/Lean/PrettyPrinter/Delaborator.lean b/src/Lean/PrettyPrinter/Delaborator.lean index 22c52d89ca..9ce24b2db7 100644 --- a/src/Lean/PrettyPrinter/Delaborator.lean +++ b/src/Lean/PrettyPrinter/Delaborator.lean @@ -11,5 +11,3 @@ public import Lean.PrettyPrinter.Delaborator.SubExpr public import Lean.PrettyPrinter.Delaborator.TopDownAnalyze public import Lean.PrettyPrinter.Delaborator.Basic public import Lean.PrettyPrinter.Delaborator.Builtins - -public section diff --git a/src/Lean/Server.lean b/src/Lean/Server.lean index d1a26f90ab..c843f8549c 100644 --- a/src/Lean/Server.lean +++ b/src/Lean/Server.lean @@ -12,5 +12,3 @@ public import Lean.Server.FileWorker public import Lean.Server.Rpc public import Lean.Server.CodeActions public import Lean.Server.Test - -public section diff --git a/src/Lean/Server/CodeActions.lean b/src/Lean/Server/CodeActions.lean index c68d5753b9..47e4b28132 100644 --- a/src/Lean/Server/CodeActions.lean +++ b/src/Lean/Server/CodeActions.lean @@ -10,5 +10,3 @@ prelude public import Lean.Server.CodeActions.Attr public import Lean.Server.CodeActions.Basic public import Lean.Server.CodeActions.Provider - -public section diff --git a/src/Lean/Server/Rpc.lean b/src/Lean/Server/Rpc.lean index 44782b41f7..09e569a08a 100644 --- a/src/Lean/Server/Rpc.lean +++ b/src/Lean/Server/Rpc.lean @@ -10,5 +10,3 @@ prelude public import Lean.Server.Rpc.Basic public import Lean.Server.Rpc.Deriving public import Lean.Server.Rpc.RequestHandling - -public section diff --git a/src/Lean/Server/Test.lean b/src/Lean/Server/Test.lean index 4dd4c25460..ac25877283 100644 --- a/src/Lean/Server/Test.lean +++ b/src/Lean/Server/Test.lean @@ -10,5 +10,3 @@ prelude public import Lean.Server.Test.Cancel public import Lean.Server.Test.Runner public import Lean.Server.Test.Refs - -public section diff --git a/src/Lean/Util.lean b/src/Lean/Util.lean index 304b078ff6..3f9161046d 100644 --- a/src/Lean/Util.lean +++ b/src/Lean/Util.lean @@ -38,5 +38,3 @@ public import Lean.Util.NumApps public import Lean.Util.FVarSubset public import Lean.Util.SortExprs public import Lean.Util.Reprove - -public section diff --git a/src/Lean/Widget.lean b/src/Lean/Widget.lean index b5766422ed..d9a3c6b868 100644 --- a/src/Lean/Widget.lean +++ b/src/Lean/Widget.lean @@ -13,5 +13,3 @@ public import Lean.Widget.InteractiveGoal public import Lean.Widget.TaggedText public import Lean.Widget.UserWidget public import Lean.Widget.Commands - -public section diff --git a/src/Std/Data.lean b/src/Std/Data.lean index d602fdda4d..0479b505e7 100644 --- a/src/Std/Data.lean +++ b/src/Std/Data.lean @@ -31,5 +31,3 @@ public import Std.Data.TreeSet.Raw public import Std.Data.Iterators public import Std.Data.ByteSlice - -@[expose] public section diff --git a/src/Std/Data/DHashMap.lean b/src/Std/Data/DHashMap.lean index 29763dff90..937ca58850 100644 --- a/src/Std/Data/DHashMap.lean +++ b/src/Std/Data/DHashMap.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.DHashMap.Basic public import Std.Data.DHashMap.Lemmas public import Std.Data.DHashMap.AdditionalOperations - -public section diff --git a/src/Std/Data/DTreeMap.lean b/src/Std/Data/DTreeMap.lean index b9f1a76248..41af848340 100644 --- a/src/Std/Data/DTreeMap.lean +++ b/src/Std/Data/DTreeMap.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.DTreeMap.Basic public import Std.Data.DTreeMap.AdditionalOperations public import Std.Data.DTreeMap.Lemmas - -@[expose] public section diff --git a/src/Std/Data/DTreeMap/Raw.lean b/src/Std/Data/DTreeMap/Raw.lean index 5f13cb0064..4fe19c0a64 100644 --- a/src/Std/Data/DTreeMap/Raw.lean +++ b/src/Std/Data/DTreeMap/Raw.lean @@ -10,5 +10,3 @@ public import Std.Data.DTreeMap.Raw.Basic public import Std.Data.DTreeMap.Raw.AdditionalOperations public import Std.Data.DTreeMap.Raw.Lemmas public import Std.Data.DTreeMap.Raw.WF - -@[expose] public section diff --git a/src/Std/Data/ExtDHashMap.lean b/src/Std/Data/ExtDHashMap.lean index a63cd1e7b0..2830bb050c 100644 --- a/src/Std/Data/ExtDHashMap.lean +++ b/src/Std/Data/ExtDHashMap.lean @@ -8,5 +8,3 @@ module prelude public import Std.Data.ExtDHashMap.Basic public import Std.Data.ExtDHashMap.Lemmas - -@[expose] public section diff --git a/src/Std/Data/ExtDTreeMap.lean b/src/Std/Data/ExtDTreeMap.lean index 2dd54e12fa..76684cdd38 100644 --- a/src/Std/Data/ExtDTreeMap.lean +++ b/src/Std/Data/ExtDTreeMap.lean @@ -8,5 +8,3 @@ module prelude public import Std.Data.ExtDTreeMap.Basic public import Std.Data.ExtDTreeMap.Lemmas - -@[expose] public section diff --git a/src/Std/Data/ExtHashMap.lean b/src/Std/Data/ExtHashMap.lean index 8ef6ff7160..34110e1cf6 100644 --- a/src/Std/Data/ExtHashMap.lean +++ b/src/Std/Data/ExtHashMap.lean @@ -8,5 +8,3 @@ module prelude public import Std.Data.ExtHashMap.Basic public import Std.Data.ExtHashMap.Lemmas - -@[expose] public section diff --git a/src/Std/Data/ExtHashSet.lean b/src/Std/Data/ExtHashSet.lean index a828b4e82c..eaede3f865 100644 --- a/src/Std/Data/ExtHashSet.lean +++ b/src/Std/Data/ExtHashSet.lean @@ -8,5 +8,3 @@ module prelude public import Std.Data.ExtHashSet.Basic public import Std.Data.ExtHashSet.Lemmas - -@[expose] public section diff --git a/src/Std/Data/ExtTreeMap.lean b/src/Std/Data/ExtTreeMap.lean index 4fa507cdac..12176e5d1a 100644 --- a/src/Std/Data/ExtTreeMap.lean +++ b/src/Std/Data/ExtTreeMap.lean @@ -8,5 +8,3 @@ module prelude public import Std.Data.ExtTreeMap.Basic public import Std.Data.ExtTreeMap.Lemmas - -@[expose] public section diff --git a/src/Std/Data/ExtTreeSet.lean b/src/Std/Data/ExtTreeSet.lean index ce7a980e64..fb62ee410a 100644 --- a/src/Std/Data/ExtTreeSet.lean +++ b/src/Std/Data/ExtTreeSet.lean @@ -8,5 +8,3 @@ module prelude public import Std.Data.ExtTreeSet.Basic public import Std.Data.ExtTreeSet.Lemmas - -@[expose] public section diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index 7fe186198e..f86b6bfe18 100644 --- a/src/Std/Data/HashMap.lean +++ b/src/Std/Data/HashMap.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.HashMap.Basic public import Std.Data.HashMap.Lemmas public import Std.Data.HashMap.AdditionalOperations - -@[expose] public section diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean index 5dfbcb19b6..0e404fbc3d 100644 --- a/src/Std/Data/HashSet.lean +++ b/src/Std/Data/HashSet.lean @@ -8,5 +8,3 @@ module prelude public import Std.Data.HashSet.Basic public import Std.Data.HashSet.Lemmas - -@[expose] public section diff --git a/src/Std/Data/Iterators/Combinators.lean b/src/Std/Data/Iterators/Combinators.lean index cfcbfb1c43..72dd74b6f8 100644 --- a/src/Std/Data/Iterators/Combinators.lean +++ b/src/Std/Data/Iterators/Combinators.lean @@ -13,5 +13,3 @@ public import Std.Data.Iterators.Combinators.Drop public import Std.Data.Iterators.Combinators.DropWhile public import Std.Data.Iterators.Combinators.StepSize public import Std.Data.Iterators.Combinators.Zip - -@[expose] public section diff --git a/src/Std/Data/Iterators/Combinators/Monadic.lean b/src/Std/Data/Iterators/Combinators/Monadic.lean index 9002dd9896..e4c93bbac5 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic.lean @@ -12,5 +12,3 @@ public import Std.Data.Iterators.Combinators.Monadic.Drop public import Std.Data.Iterators.Combinators.Monadic.DropWhile public import Std.Data.Iterators.Combinators.Monadic.StepSize public import Std.Data.Iterators.Combinators.Monadic.Zip - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas.lean b/src/Std/Data/Iterators/Lemmas.lean index b9fc184687..8e0eee3173 100644 --- a/src/Std/Data/Iterators/Lemmas.lean +++ b/src/Std/Data/Iterators/Lemmas.lean @@ -11,5 +11,3 @@ public import Std.Data.Iterators.Lemmas.Monadic public import Std.Data.Iterators.Lemmas.Combinators public import Std.Data.Iterators.Lemmas.Producers public import Std.Data.Iterators.Lemmas.Equivalence - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas/Combinators.lean b/src/Std/Data/Iterators/Lemmas/Combinators.lean index afab571421..25938cf8b9 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators.lean @@ -12,5 +12,3 @@ public import Std.Data.Iterators.Lemmas.Combinators.TakeWhile public import Std.Data.Iterators.Lemmas.Combinators.Drop public import Std.Data.Iterators.Lemmas.Combinators.DropWhile public import Std.Data.Iterators.Lemmas.Combinators.Zip - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean index 36aba5ff4c..bb8fc58bd7 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean @@ -12,5 +12,3 @@ public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop public import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile public import Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas/Consumers.lean b/src/Std/Data/Iterators/Lemmas/Consumers.lean index dd4f503bae..0c40646fbb 100644 --- a/src/Std/Data/Iterators/Lemmas/Consumers.lean +++ b/src/Std/Data/Iterators/Lemmas/Consumers.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.Iterators.Lemmas.Consumers.Monadic public import Std.Data.Iterators.Lemmas.Consumers.Collect public import Std.Data.Iterators.Lemmas.Consumers.Loop - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean index cd20111e05..5c8d58c4b6 100644 --- a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean +++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean @@ -8,5 +8,3 @@ module prelude public import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect public import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence.lean b/src/Std/Data/Iterators/Lemmas/Equivalence.lean index f18f6bee08..4448929609 100644 --- a/src/Std/Data/Iterators/Lemmas/Equivalence.lean +++ b/src/Std/Data/Iterators/Lemmas/Equivalence.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.Iterators.Lemmas.Equivalence.HetT public import Std.Data.Iterators.Lemmas.Equivalence.Basic public import Std.Data.Iterators.Lemmas.Equivalence.StepCongr - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Monadic.lean index 60d1bf8438..228c36340f 100644 --- a/src/Std/Data/Iterators/Lemmas/Monadic.lean +++ b/src/Std/Data/Iterators/Lemmas/Monadic.lean @@ -7,5 +7,3 @@ module prelude public import Init.Data.Iterators.Lemmas.Monadic.Basic - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas/Producers.lean b/src/Std/Data/Iterators/Lemmas/Producers.lean index 5aec327479..eb164a7ff0 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers.lean @@ -13,5 +13,3 @@ public import Std.Data.Iterators.Lemmas.Producers.List public import Std.Data.Iterators.Lemmas.Producers.Repeat public import Std.Data.Iterators.Lemmas.Producers.Range public import Std.Data.Iterators.Lemmas.Producers.Slice - -@[expose] public section diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean index 9943e9054a..50904ce584 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.Iterators.Lemmas.Producers.Monadic.Array public import Std.Data.Iterators.Lemmas.Producers.Monadic.Empty public import Std.Data.Iterators.Lemmas.Producers.Monadic.List - -@[expose] public section diff --git a/src/Std/Data/Iterators/Producers.lean b/src/Std/Data/Iterators/Producers.lean index 5475f12e7b..d5d6c4ab95 100644 --- a/src/Std/Data/Iterators/Producers.lean +++ b/src/Std/Data/Iterators/Producers.lean @@ -13,5 +13,3 @@ public import Std.Data.Iterators.Producers.List public import Std.Data.Iterators.Producers.Range public import Std.Data.Iterators.Producers.Repeat public import Std.Data.Iterators.Producers.Slice - -@[expose] public section diff --git a/src/Std/Data/Iterators/Producers/Monadic.lean b/src/Std/Data/Iterators/Producers/Monadic.lean index e90a6140f5..1f80e13bd1 100644 --- a/src/Std/Data/Iterators/Producers/Monadic.lean +++ b/src/Std/Data/Iterators/Producers/Monadic.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.Iterators.Producers.Monadic.Array public import Std.Data.Iterators.Producers.Monadic.Empty public import Std.Data.Iterators.Producers.Monadic.List - -@[expose] public section diff --git a/src/Std/Data/TreeMap.lean b/src/Std/Data/TreeMap.lean index a82e5d9eab..ab1ab33cf2 100644 --- a/src/Std/Data/TreeMap.lean +++ b/src/Std/Data/TreeMap.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.TreeMap.Basic public import Std.Data.TreeMap.AdditionalOperations public import Std.Data.TreeMap.Lemmas - -@[expose] public section diff --git a/src/Std/Data/TreeMap/Raw.lean b/src/Std/Data/TreeMap/Raw.lean index 52bff67b7f..70622beb57 100644 --- a/src/Std/Data/TreeMap/Raw.lean +++ b/src/Std/Data/TreeMap/Raw.lean @@ -10,5 +10,3 @@ public import Std.Data.TreeMap.Raw.Basic public import Std.Data.TreeMap.Raw.AdditionalOperations public import Std.Data.TreeMap.Raw.Lemmas public import Std.Data.TreeMap.Raw.WF - -@[expose] public section diff --git a/src/Std/Data/TreeSet.lean b/src/Std/Data/TreeSet.lean index 9cfd575519..82c304bea0 100644 --- a/src/Std/Data/TreeSet.lean +++ b/src/Std/Data/TreeSet.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.TreeSet.Basic public import Std.Data.TreeSet.AdditionalOperations public import Std.Data.TreeSet.Lemmas - -@[expose] public section diff --git a/src/Std/Data/TreeSet/Raw.lean b/src/Std/Data/TreeSet/Raw.lean index 8035c0c4e7..6aaf9a23eb 100644 --- a/src/Std/Data/TreeSet/Raw.lean +++ b/src/Std/Data/TreeSet/Raw.lean @@ -9,5 +9,3 @@ prelude public import Std.Data.TreeSet.Raw.Basic public import Std.Data.TreeSet.Raw.Lemmas public import Std.Data.TreeSet.Raw.WF - -@[expose] public section diff --git a/src/Std/Do.lean b/src/Std/Do.lean index ccf190a106..d0430fc1b9 100644 --- a/src/Std/Do.lean +++ b/src/Std/Do.lean @@ -11,5 +11,3 @@ public import Std.Do.WP public import Std.Do.Triple public import Std.Do.PredTrans public import Std.Do.PostCond - -@[expose] public section diff --git a/src/Std/Do/SPred.lean b/src/Std/Do/SPred.lean index 982f2e3478..383409a965 100644 --- a/src/Std/Do/SPred.lean +++ b/src/Std/Do/SPred.lean @@ -11,5 +11,3 @@ public import Std.Do.SPred.SPred public import Std.Do.SPred.Notation public import Std.Do.SPred.Laws public import Std.Do.SPred.DerivedLaws - -@[expose] public section diff --git a/src/Std/Do/Triple.lean b/src/Std/Do/Triple.lean index 0d9456288f..85362ca900 100644 --- a/src/Std/Do/Triple.lean +++ b/src/Std/Do/Triple.lean @@ -8,5 +8,3 @@ module prelude public import Std.Do.Triple.Basic public import Std.Do.Triple.SpecLemmas - -@[expose] public section diff --git a/src/Std/Do/WP.lean b/src/Std/Do/WP.lean index be1d2d0da3..3307893123 100644 --- a/src/Std/Do/WP.lean +++ b/src/Std/Do/WP.lean @@ -10,5 +10,3 @@ public import Std.Do.WP.Basic public import Std.Do.WP.Monad public import Std.Do.WP.IO public import Std.Do.WP.SimpLemmas - -@[expose] public section diff --git a/src/Std/Internal/Async.lean b/src/Std/Internal/Async.lean index d17797a266..1d7954fd16 100644 --- a/src/Std/Internal/Async.lean +++ b/src/Std/Internal/Async.lean @@ -16,5 +16,3 @@ public import Std.Internal.Async.Process public import Std.Internal.Async.System public import Std.Internal.Async.Signal public import Std.Internal.Async.IO - -public section diff --git a/src/Std/Internal/Parsec.lean b/src/Std/Internal/Parsec.lean index 019a921031..3d83d49c94 100644 --- a/src/Std/Internal/Parsec.lean +++ b/src/Std/Internal/Parsec.lean @@ -9,5 +9,3 @@ prelude public import Std.Internal.Parsec.Basic public import Std.Internal.Parsec.String public import Std.Internal.Parsec.ByteArray - -public section diff --git a/src/Std/Internal/UV.lean b/src/Std/Internal/UV.lean index 1b829426cf..c3c42f19d3 100644 --- a/src/Std/Internal/UV.lean +++ b/src/Std/Internal/UV.lean @@ -16,5 +16,3 @@ public import Std.Internal.UV.UDP public import Std.Internal.UV.System public import Std.Internal.UV.DNS public import Std.Internal.UV.Signal - -@[expose] public section diff --git a/src/Std/Net.lean b/src/Std/Net.lean index d0c7caec77..fee06875f7 100644 --- a/src/Std/Net.lean +++ b/src/Std/Net.lean @@ -7,5 +7,3 @@ module prelude public import Std.Net.Addr - -@[expose] public section diff --git a/src/Std/Sat.lean b/src/Std/Sat.lean index 65fbafdac1..34e6ef1a5b 100644 --- a/src/Std/Sat.lean +++ b/src/Std/Sat.lean @@ -8,5 +8,3 @@ module prelude public import Std.Sat.AIG public import Std.Sat.CNF - -@[expose] public section diff --git a/src/Std/Sat/AIG.lean b/src/Std/Sat/AIG.lean index 663f9695b5..291793f80c 100644 --- a/src/Std/Sat/AIG.lean +++ b/src/Std/Sat/AIG.lean @@ -20,5 +20,3 @@ public import Std.Sat.AIG.RefVec public import Std.Sat.AIG.RefVecOperator public import Std.Sat.AIG.LawfulVecOperator public import Std.Sat.AIG.If - -@[expose] public section diff --git a/src/Std/Sat/AIG/RefVecOperator.lean b/src/Std/Sat/AIG/RefVecOperator.lean index c117278edf..77d78c7d1b 100644 --- a/src/Std/Sat/AIG/RefVecOperator.lean +++ b/src/Std/Sat/AIG/RefVecOperator.lean @@ -9,5 +9,3 @@ prelude public import Std.Sat.AIG.RefVecOperator.Map public import Std.Sat.AIG.RefVecOperator.Zip public import Std.Sat.AIG.RefVecOperator.Fold - -@[expose] public section diff --git a/src/Std/Sat/CNF.lean b/src/Std/Sat/CNF.lean index 9a7a7f88f5..5911e28e08 100644 --- a/src/Std/Sat/CNF.lean +++ b/src/Std/Sat/CNF.lean @@ -11,5 +11,3 @@ public import Std.Sat.CNF.Literal public import Std.Sat.CNF.Relabel public import Std.Sat.CNF.RelabelFin public import Std.Sat.CNF.Dimacs - -@[expose] public section diff --git a/src/Std/Sync.lean b/src/Std/Sync.lean index 410b8d1fe0..b637ae0763 100644 --- a/src/Std/Sync.lean +++ b/src/Std/Sync.lean @@ -13,5 +13,3 @@ public import Std.Sync.RecursiveMutex public import Std.Sync.Barrier public import Std.Sync.SharedMutex public import Std.Sync.Notify - -@[expose] public section diff --git a/src/Std/Time/Date.lean b/src/Std/Time/Date.lean index 4886df833e..5c451f8cf7 100644 --- a/src/Std/Time/Date.lean +++ b/src/Std/Time/Date.lean @@ -8,5 +8,3 @@ module prelude public import Std.Time.Date.Basic public import Std.Time.Date.PlainDate - -public section diff --git a/src/Std/Time/Internal.lean b/src/Std/Time/Internal.lean index d7c3edff68..7f62df4fff 100644 --- a/src/Std/Time/Internal.lean +++ b/src/Std/Time/Internal.lean @@ -8,5 +8,3 @@ module prelude public import Std.Time.Internal.Bounded public import Std.Time.Internal.UnitVal - -public section diff --git a/src/Std/Time/Time.lean b/src/Std/Time/Time.lean index 6594115c9e..963838dceb 100644 --- a/src/Std/Time/Time.lean +++ b/src/Std/Time/Time.lean @@ -9,5 +9,3 @@ prelude public import Std.Time.Time.Basic public import Std.Time.Time.HourMarker public import Std.Time.Time.PlainTime - -public section diff --git a/src/Std/Time/Time/Basic.lean b/src/Std/Time/Time/Basic.lean index 4fdd3853b7..bc9aea7ac8 100644 --- a/src/Std/Time/Time/Basic.lean +++ b/src/Std/Time/Time/Basic.lean @@ -7,5 +7,3 @@ module prelude public import Std.Time.Time.Unit.Basic - -public section