From 7feb583b9e4ca5b2958f993a578d4bd9d8ca3f48 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 23 Apr 2025 19:21:33 +0200 Subject: [PATCH] feat: enable experimental module system in `Init` (#8047) --- src/Init/BinderNameHint.lean | 2 ++ src/Init/BinderPredicates.lean | 2 ++ src/Init/ByCases.lean | 2 ++ src/Init/Classical.lean | 2 ++ src/Init/Coe.lean | 2 ++ src/Init/Control.lean | 2 ++ src/Init/Control/Basic.lean | 2 ++ src/Init/Control/EState.lean | 2 ++ src/Init/Control/Except.lean | 2 ++ src/Init/Control/ExceptCps.lean | 2 ++ src/Init/Control/Id.lean | 2 ++ src/Init/Control/Lawful.lean | 2 ++ src/Init/Control/Lawful/Basic.lean | 2 ++ src/Init/Control/Lawful/Instances.lean | 2 ++ src/Init/Control/Lawful/Lemmas.lean | 2 ++ src/Init/Control/Option.lean | 2 ++ src/Init/Control/Reader.lean | 2 ++ src/Init/Control/State.lean | 2 ++ src/Init/Control/StateCps.lean | 2 ++ src/Init/Control/StateRef.lean | 2 ++ src/Init/Conv.lean | 2 ++ src/Init/Core.lean | 2 ++ src/Init/Data.lean | 2 ++ src/Init/Data/AC.lean | 2 ++ src/Init/Data/Array.lean | 2 ++ src/Init/Data/Array/Attach.lean | 2 ++ src/Init/Data/Array/Basic.lean | 2 ++ src/Init/Data/Array/BasicAux.lean | 2 ++ src/Init/Data/Array/BinSearch.lean | 2 ++ src/Init/Data/Array/Bootstrap.lean | 2 ++ src/Init/Data/Array/Count.lean | 2 ++ src/Init/Data/Array/DecidableEq.lean | 2 ++ src/Init/Data/Array/Erase.lean | 2 ++ src/Init/Data/Array/Extract.lean | 2 ++ src/Init/Data/Array/FinRange.lean | 2 ++ src/Init/Data/Array/Find.lean | 2 ++ src/Init/Data/Array/GetLit.lean | 2 ++ src/Init/Data/Array/InsertIdx.lean | 2 ++ src/Init/Data/Array/InsertionSort.lean | 2 ++ src/Init/Data/Array/Lemmas.lean | 2 ++ src/Init/Data/Array/Lex.lean | 2 ++ src/Init/Data/Array/Lex/Basic.lean | 2 ++ src/Init/Data/Array/Lex/Lemmas.lean | 2 ++ src/Init/Data/Array/MapIdx.lean | 2 ++ src/Init/Data/Array/Mem.lean | 2 ++ src/Init/Data/Array/Monadic.lean | 2 ++ src/Init/Data/Array/OfFn.lean | 2 ++ src/Init/Data/Array/Perm.lean | 2 ++ src/Init/Data/Array/QSort.lean | 2 ++ src/Init/Data/Array/Range.lean | 2 ++ src/Init/Data/Array/Set.lean | 2 ++ src/Init/Data/Array/Subarray.lean | 2 ++ src/Init/Data/Array/Subarray/Split.lean | 2 ++ src/Init/Data/Array/TakeDrop.lean | 2 ++ src/Init/Data/Array/Zip.lean | 2 ++ src/Init/Data/BEq.lean | 2 ++ src/Init/Data/Basic.lean | 2 ++ src/Init/Data/BitVec.lean | 2 ++ src/Init/Data/BitVec/Basic.lean | 2 ++ src/Init/Data/BitVec/BasicAux.lean | 2 ++ src/Init/Data/BitVec/Bitblast.lean | 2 ++ src/Init/Data/BitVec/Folds.lean | 2 ++ src/Init/Data/BitVec/Lemmas.lean | 2 ++ src/Init/Data/Bool.lean | 2 ++ src/Init/Data/ByteArray.lean | 2 ++ src/Init/Data/ByteArray/Basic.lean | 2 ++ src/Init/Data/Cast.lean | 2 ++ src/Init/Data/Char.lean | 2 ++ src/Init/Data/Char/Basic.lean | 2 ++ src/Init/Data/Char/Lemmas.lean | 2 ++ src/Init/Data/Fin.lean | 2 ++ src/Init/Data/Fin/Basic.lean | 2 ++ src/Init/Data/Fin/Bitwise.lean | 2 ++ src/Init/Data/Fin/Fold.lean | 2 ++ src/Init/Data/Fin/Iterate.lean | 2 ++ src/Init/Data/Fin/Lemmas.lean | 2 ++ src/Init/Data/Fin/Log2.lean | 2 ++ src/Init/Data/Float.lean | 2 ++ src/Init/Data/Float32.lean | 2 ++ src/Init/Data/FloatArray.lean | 2 ++ src/Init/Data/FloatArray/Basic.lean | 2 ++ src/Init/Data/Format.lean | 2 ++ src/Init/Data/Format/Basic.lean | 2 ++ src/Init/Data/Format/Instances.lean | 2 ++ src/Init/Data/Format/Macro.lean | 2 ++ src/Init/Data/Format/Syntax.lean | 2 ++ src/Init/Data/Function.lean | 2 ++ src/Init/Data/Hashable.lean | 2 ++ src/Init/Data/Int.lean | 2 ++ src/Init/Data/Int/Basic.lean | 2 ++ src/Init/Data/Int/Bitwise.lean | 2 ++ src/Init/Data/Int/Bitwise/Basic.lean | 2 ++ src/Init/Data/Int/Bitwise/Lemmas.lean | 2 ++ src/Init/Data/Int/Compare.lean | 2 ++ src/Init/Data/Int/Cooper.lean | 2 ++ src/Init/Data/Int/DivMod.lean | 2 ++ src/Init/Data/Int/DivMod/Basic.lean | 2 ++ src/Init/Data/Int/DivMod/Bootstrap.lean | 2 ++ src/Init/Data/Int/DivMod/Lemmas.lean | 2 ++ src/Init/Data/Int/Gcd.lean | 2 ++ src/Init/Data/Int/Lemmas.lean | 2 ++ src/Init/Data/Int/LemmasAux.lean | 2 ++ src/Init/Data/Int/Linear.lean | 2 ++ src/Init/Data/Int/OfNat.lean | 2 ++ src/Init/Data/Int/Order.lean | 2 ++ src/Init/Data/Int/Pow.lean | 2 ++ src/Init/Data/List.lean | 2 ++ src/Init/Data/List/Attach.lean | 2 ++ src/Init/Data/List/Basic.lean | 2 ++ src/Init/Data/List/BasicAux.lean | 2 ++ src/Init/Data/List/Control.lean | 2 ++ src/Init/Data/List/Count.lean | 2 ++ src/Init/Data/List/Erase.lean | 2 ++ src/Init/Data/List/FinRange.lean | 2 ++ src/Init/Data/List/Find.lean | 2 ++ src/Init/Data/List/Impl.lean | 2 ++ src/Init/Data/List/Lemmas.lean | 2 ++ src/Init/Data/List/Lex.lean | 2 ++ src/Init/Data/List/MapIdx.lean | 2 ++ src/Init/Data/List/MinMax.lean | 2 ++ src/Init/Data/List/Monadic.lean | 2 ++ src/Init/Data/List/Nat.lean | 2 ++ src/Init/Data/List/Nat/BEq.lean | 2 ++ src/Init/Data/List/Nat/Basic.lean | 2 ++ src/Init/Data/List/Nat/Count.lean | 2 ++ src/Init/Data/List/Nat/Erase.lean | 2 ++ src/Init/Data/List/Nat/Find.lean | 2 ++ src/Init/Data/List/Nat/InsertIdx.lean | 2 ++ src/Init/Data/List/Nat/Modify.lean | 2 ++ src/Init/Data/List/Nat/Pairwise.lean | 2 ++ src/Init/Data/List/Nat/Perm.lean | 2 ++ src/Init/Data/List/Nat/Range.lean | 2 ++ src/Init/Data/List/Nat/Sublist.lean | 2 ++ src/Init/Data/List/Nat/TakeDrop.lean | 2 ++ src/Init/Data/List/Notation.lean | 2 ++ src/Init/Data/List/OfFn.lean | 2 ++ src/Init/Data/List/Pairwise.lean | 2 ++ src/Init/Data/List/Perm.lean | 2 ++ src/Init/Data/List/Range.lean | 2 ++ src/Init/Data/List/Sort.lean | 2 ++ src/Init/Data/List/Sort/Basic.lean | 2 ++ src/Init/Data/List/Sort/Impl.lean | 2 ++ src/Init/Data/List/Sort/Lemmas.lean | 2 ++ src/Init/Data/List/Sublist.lean | 2 ++ src/Init/Data/List/TakeDrop.lean | 2 ++ src/Init/Data/List/ToArray.lean | 2 ++ src/Init/Data/List/ToArrayImpl.lean | 2 ++ src/Init/Data/List/Zip.lean | 2 ++ src/Init/Data/Nat.lean | 2 ++ src/Init/Data/Nat/Basic.lean | 2 ++ src/Init/Data/Nat/Bitwise.lean | 2 ++ src/Init/Data/Nat/Bitwise/Basic.lean | 2 ++ src/Init/Data/Nat/Bitwise/Lemmas.lean | 2 ++ src/Init/Data/Nat/Compare.lean | 2 ++ src/Init/Data/Nat/Control.lean | 2 ++ src/Init/Data/Nat/Div.lean | 2 ++ src/Init/Data/Nat/Div/Basic.lean | 2 ++ src/Init/Data/Nat/Div/Lemmas.lean | 2 ++ src/Init/Data/Nat/Dvd.lean | 2 ++ src/Init/Data/Nat/Fold.lean | 2 ++ src/Init/Data/Nat/Gcd.lean | 2 ++ src/Init/Data/Nat/Lcm.lean | 2 ++ src/Init/Data/Nat/Lemmas.lean | 2 ++ src/Init/Data/Nat/Linear.lean | 2 ++ src/Init/Data/Nat/Log2.lean | 2 ++ src/Init/Data/Nat/MinMax.lean | 2 ++ src/Init/Data/Nat/Mod.lean | 2 ++ src/Init/Data/Nat/Power2.lean | 2 ++ src/Init/Data/Nat/SOM.lean | 2 ++ src/Init/Data/Nat/Simproc.lean | 2 ++ src/Init/Data/NeZero.lean | 2 ++ src/Init/Data/OfScientific.lean | 2 ++ src/Init/Data/Option.lean | 2 ++ src/Init/Data/Option/Attach.lean | 2 ++ src/Init/Data/Option/Basic.lean | 2 ++ src/Init/Data/Option/BasicAux.lean | 2 ++ src/Init/Data/Option/Instances.lean | 2 ++ src/Init/Data/Option/Lemmas.lean | 2 ++ src/Init/Data/Option/List.lean | 2 ++ src/Init/Data/Option/Monadic.lean | 2 ++ src/Init/Data/Ord.lean | 2 ++ src/Init/Data/PLift.lean | 2 ++ src/Init/Data/Prod.lean | 2 ++ src/Init/Data/Queue.lean | 2 ++ src/Init/Data/RArray.lean | 2 ++ src/Init/Data/Random.lean | 2 ++ src/Init/Data/Range.lean | 2 ++ src/Init/Data/Range/Basic.lean | 2 ++ src/Init/Data/Range/Lemmas.lean | 2 ++ src/Init/Data/Repr.lean | 2 ++ src/Init/Data/SInt.lean | 2 ++ src/Init/Data/SInt/Basic.lean | 2 ++ src/Init/Data/SInt/Bitwise.lean | 2 ++ src/Init/Data/SInt/Float.lean | 2 ++ src/Init/Data/SInt/Float32.lean | 2 ++ src/Init/Data/SInt/Lemmas.lean | 2 ++ src/Init/Data/Stream.lean | 2 ++ src/Init/Data/String.lean | 2 ++ src/Init/Data/String/Basic.lean | 2 ++ src/Init/Data/String/Extra.lean | 2 ++ src/Init/Data/String/Lemmas.lean | 2 ++ src/Init/Data/Subtype.lean | 2 ++ src/Init/Data/Sum.lean | 2 ++ src/Init/Data/Sum/Basic.lean | 2 ++ src/Init/Data/Sum/Lemmas.lean | 2 ++ src/Init/Data/ToString.lean | 2 ++ src/Init/Data/ToString/Basic.lean | 2 ++ src/Init/Data/ToString/Macro.lean | 2 ++ src/Init/Data/UInt.lean | 2 ++ src/Init/Data/UInt/Basic.lean | 2 ++ src/Init/Data/UInt/BasicAux.lean | 2 ++ src/Init/Data/UInt/Bitwise.lean | 2 ++ src/Init/Data/UInt/Lemmas.lean | 2 ++ src/Init/Data/UInt/Log2.lean | 2 ++ src/Init/Data/ULift.lean | 2 ++ src/Init/Data/Vector.lean | 2 ++ src/Init/Data/Vector/Attach.lean | 2 ++ src/Init/Data/Vector/Basic.lean | 2 ++ src/Init/Data/Vector/Count.lean | 2 ++ src/Init/Data/Vector/DecidableEq.lean | 2 ++ src/Init/Data/Vector/Erase.lean | 2 ++ src/Init/Data/Vector/Extract.lean | 2 ++ src/Init/Data/Vector/FinRange.lean | 2 ++ src/Init/Data/Vector/Find.lean | 2 ++ src/Init/Data/Vector/InsertIdx.lean | 2 ++ src/Init/Data/Vector/Lemmas.lean | 2 ++ src/Init/Data/Vector/Lex.lean | 2 ++ src/Init/Data/Vector/MapIdx.lean | 2 ++ src/Init/Data/Vector/Monadic.lean | 2 ++ src/Init/Data/Vector/OfFn.lean | 2 ++ src/Init/Data/Vector/Perm.lean | 2 ++ src/Init/Data/Vector/Range.lean | 2 ++ src/Init/Data/Vector/Zip.lean | 2 ++ src/Init/Data/Zero.lean | 2 ++ src/Init/Dynamic.lean | 2 ++ src/Init/Ext.lean | 2 ++ src/Init/GetElem.lean | 2 ++ src/Init/Grind.lean | 2 ++ src/Init/Grind/Cases.lean | 2 ++ src/Init/Grind/CommRing.lean | 2 ++ src/Init/Grind/CommRing/Basic.lean | 2 ++ src/Init/Grind/CommRing/BitVec.lean | 2 ++ src/Init/Grind/CommRing/Int.lean | 2 ++ src/Init/Grind/CommRing/Poly.lean | 2 ++ src/Init/Grind/CommRing/SInt.lean | 2 ++ src/Init/Grind/CommRing/UInt.lean | 2 ++ src/Init/Grind/Ext.lean | 2 ++ src/Init/Grind/Lemmas.lean | 2 ++ src/Init/Grind/Norm.lean | 2 ++ src/Init/Grind/Offset.lean | 2 ++ src/Init/Grind/PP.lean | 2 ++ src/Init/Grind/Propagator.lean | 2 ++ src/Init/Grind/Tactics.lean | 2 ++ src/Init/Grind/Util.lean | 2 ++ src/Init/Guard.lean | 2 ++ src/Init/Hints.lean | 2 ++ src/Init/Internal.lean | 2 ++ src/Init/Internal/Order.lean | 2 ++ src/Init/Internal/Order/Basic.lean | 2 ++ src/Init/Internal/Order/Lemmas.lean | 2 ++ src/Init/Internal/Order/Tactic.lean | 2 ++ src/Init/MacroTrace.lean | 2 ++ src/Init/Meta.lean | 2 ++ src/Init/MetaTypes.lean | 2 ++ src/Init/Notation.lean | 2 ++ src/Init/NotationExtra.lean | 2 ++ src/Init/Omega.lean | 2 ++ src/Init/Omega/Coeffs.lean | 2 ++ src/Init/Omega/Constraint.lean | 2 ++ src/Init/Omega/Int.lean | 2 ++ src/Init/Omega/IntList.lean | 2 ++ src/Init/Omega/LinearCombo.lean | 2 ++ src/Init/Omega/Logic.lean | 2 ++ src/Init/Prelude.lean | 2 ++ src/Init/PropLemmas.lean | 2 ++ src/Init/RCases.lean | 2 ++ src/Init/ShareCommon.lean | 2 ++ src/Init/SimpLemmas.lean | 2 ++ src/Init/Simproc.lean | 2 ++ src/Init/SizeOf.lean | 2 ++ src/Init/SizeOfLemmas.lean | 2 ++ src/Init/Syntax.lean | 2 ++ src/Init/System.lean | 2 ++ src/Init/System/FilePath.lean | 2 ++ src/Init/System/IO.lean | 2 ++ src/Init/System/IOError.lean | 2 ++ src/Init/System/Mutex.lean | 2 ++ src/Init/System/Platform.lean | 2 ++ src/Init/System/Promise.lean | 2 ++ src/Init/System/ST.lean | 2 ++ src/Init/System/Uri.lean | 2 ++ src/Init/Tactics.lean | 2 ++ src/Init/TacticsExtra.lean | 2 ++ src/Init/Task.lean | 2 ++ src/Init/Try.lean | 2 ++ src/Init/Util.lean | 2 ++ src/Init/WF.lean | 2 ++ src/Init/WFTactics.lean | 2 ++ src/Init/While.lean | 2 ++ src/runtime/compact.cpp | 11 +++------- tests/bench/speedcenter.exec.velcom.yaml | 26 ++++++++++++++---------- 301 files changed, 616 insertions(+), 19 deletions(-) diff --git a/src/Init/BinderNameHint.lean b/src/Init/BinderNameHint.lean index 940168e39a..f2d5e259a8 100644 --- a/src/Init/BinderNameHint.lean +++ b/src/Init/BinderNameHint.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ +module + prelude import Init.Prelude import Init.Tactics diff --git a/src/Init/BinderPredicates.lean b/src/Init/BinderPredicates.lean index 22ad79dbb8..8640ea67b2 100644 --- a/src/Init/BinderPredicates.lean +++ b/src/Init/BinderPredicates.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ +module + prelude import Init.NotationExtra diff --git a/src/Init/ByCases.lean b/src/Init/ByCases.lean index 6e0a218419..1396f9e953 100644 --- a/src/Init/ByCases.lean +++ b/src/Init/ByCases.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Classical diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index f00e1b34ef..bd12fb48fa 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.PropLemmas diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean index 4e6adaed0f..46b7c82b65 100644 --- a/src/Init/Coe.lean +++ b/src/Init/Coe.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Prelude set_option linter.missingDocs true -- keep it documented diff --git a/src/Init/Control.lean b/src/Init/Control.lean index ab783f3634..dd3668561a 100644 --- a/src/Init/Control.lean +++ b/src/Init/Control.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Control.Basic import Init.Control.State diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index 3db848236b..94751c179e 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura, Sebastian Ullrich -/ +module + prelude import Init.Core import Init.BinderNameHint diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index db3edd97b2..4ebad9a7d9 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Control.State import Init.Control.Except diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 1ee7ec24ec..e9d7f30035 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -5,6 +5,8 @@ Authors: Jared Roesch, Sebastian Ullrich The Except monad transformer. -/ +module + prelude import Init.Control.Basic import Init.Control.Id diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean index b9f5067eb4..3fb22e9eb7 100644 --- a/src/Init/Control/ExceptCps.lean +++ b/src/Init/Control/ExceptCps.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Control.Lawful.Basic diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean index 50a494095e..eb72b1dfbc 100644 --- a/src/Init/Control/Id.lean +++ b/src/Init/Control/Id.lean @@ -5,6 +5,8 @@ Authors: Sebastian Ullrich The identity Monad. -/ +module + prelude import Init.Core diff --git a/src/Init/Control/Lawful.lean b/src/Init/Control/Lawful.lean index 80bb869e0d..fe85cc1c3f 100644 --- a/src/Init/Control/Lawful.lean +++ b/src/Init/Control/Lawful.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Control.Lawful.Basic import Init.Control.Lawful.Instances diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index b20c6769f6..8e23fd4289 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.SimpLemmas import Init.Meta diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean index 82176858c2..68f17d11f1 100644 --- a/src/Init/Control/Lawful/Instances.lean +++ b/src/Init/Control/Lawful/Instances.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Control.Lawful.Basic import Init.Control.Except diff --git a/src/Init/Control/Lawful/Lemmas.lean b/src/Init/Control/Lawful/Lemmas.lean index 5dfdd1e6e6..90fefe337b 100644 --- a/src/Init/Control/Lawful/Lemmas.lean +++ b/src/Init/Control/Lawful/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Control.Lawful.Basic import Init.RCases diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index c7ae74dc55..60b866da92 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ +module + prelude import Init.Data.Option.Basic import Init.Control.Basic diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean index a879cd8ded..ed59cb61ef 100644 --- a/src/Init/Control/Reader.lean +++ b/src/Init/Control/Reader.lean @@ -5,6 +5,8 @@ Authors: Sebastian Ullrich The Reader monad transformer for passing immutable State. -/ +module + prelude import Init.Control.Basic import Init.Control.Id diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index 3c76f52bd4..711a7311a3 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich The State monad transformer. -/ +module + prelude import Init.Control.Basic import Init.Control.Id diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean index 88229328d5..35a9fd9136 100644 --- a/src/Init/Control/StateCps.lean +++ b/src/Init/Control/StateCps.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Control.Lawful.Basic diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean index 7ed4edabf3..1a9999ac6c 100644 --- a/src/Init/Control/StateRef.lean +++ b/src/Init/Control/StateRef.lean @@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich The State monad transformer using IO references. -/ +module + prelude import Init.System.ST diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index ddb769fabe..02aa32b17f 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -5,6 +5,8 @@ Authors: Leonardo de Moura Notation for operators defined at Prelude.lean -/ +module + prelude import Init.Tactics import Init.Meta diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 6d23506397..797e1b024f 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -5,6 +5,8 @@ Authors: Leonardo de Moura notation, basic datatypes and type classes -/ +module + prelude import Init.Prelude import Init.SizeOf diff --git a/src/Init/Data.lean b/src/Init/Data.lean index 361256e2f8..4b571eae65 100644 --- a/src/Init/Data.lean +++ b/src/Init/Data.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Basic import Init.Data.Nat diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean index 29aad6ab5c..6a527598fd 100644 --- a/src/Init/Data/AC.lean +++ b/src/Init/Data/AC.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Dany Fabian -/ +module + prelude import Init.Classical import Init.ByCases diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean index e8e1ef1277..2b3259b596 100644 --- a/src/Init/Data/Array.lean +++ b/src/Init/Data/Array.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ +module + prelude import Init.Data.Array.Basic import Init.Data.Array.QSort diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean index 46a02c8d74..27683c3ab0 100644 --- a/src/Init/Data/Array/Attach.lean +++ b/src/Init/Data/Array/Attach.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner, Mario Carneiro -/ +module + prelude import Init.Data.Array.Mem import Init.Data.Array.Lemmas diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 0b6410ed1f..6ba7bed354 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.WFTactics import Init.Data.Nat.Basic diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean index 63f15838b0..159257664d 100644 --- a/src/Init/Data/Array/BasicAux.lean +++ b/src/Init/Data/Array/BasicAux.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Basic import Init.Data.Nat.Linear diff --git a/src/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean index 9c5b2668df..a900e6ba15 100644 --- a/src/Init/Data/Array/BinSearch.lean +++ b/src/Init/Data/Array/BinSearch.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Basic import Init.Data.Int.DivMod.Lemmas diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index 0a377630ab..86c240381c 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + prelude import Init.Data.List.TakeDrop diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean index e8b3faa68d..603eead158 100644 --- a/src/Init/Data/Array/Count.lean +++ b/src/Init/Data/Array/Count.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.List.Nat.Count diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index 03aa62f6b6..bdbbc511ca 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Basic import Init.Data.BEq diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean index 72bbfcc39b..372b4570f7 100644 --- a/src/Init/Data/Array/Erase.lean +++ b/src/Init/Data/Array/Erase.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.List.Nat.Erase diff --git a/src/Init/Data/Array/Extract.lean b/src/Init/Data/Array/Extract.lean index 1fe13bcdc8..d15574b874 100644 --- a/src/Init/Data/Array/Extract.lean +++ b/src/Init/Data/Array/Extract.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.List.Nat.TakeDrop diff --git a/src/Init/Data/Array/FinRange.lean b/src/Init/Data/Array/FinRange.lean index 6b7114d4fa..f3ce1afa8c 100644 --- a/src/Init/Data/Array/FinRange.lean +++ b/src/Init/Data/Array/FinRange.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 François G. Dorais. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: François G. Dorais -/ +module + prelude import Init.Data.List.FinRange import Init.Data.Array.OfFn diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index 0a2399977d..1d19296092 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Nat.Find import Init.Data.Array.Lemmas diff --git a/src/Init/Data/Array/GetLit.lean b/src/Init/Data/Array/GetLit.lean index 6ca9c20415..f98cd76a1f 100644 --- a/src/Init/Data/Array/GetLit.lean +++ b/src/Init/Data/Array/GetLit.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Basic diff --git a/src/Init/Data/Array/InsertIdx.lean b/src/Init/Data/Array/InsertIdx.lean index 3c853cfed6..2e3415b7c5 100644 --- a/src/Init/Data/Array/InsertIdx.lean +++ b/src/Init/Data/Array/InsertIdx.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.List.Nat.InsertIdx diff --git a/src/Init/Data/Array/InsertionSort.lean b/src/Init/Data/Array/InsertionSort.lean index 5ea2c62ecc..9b2dd6c950 100644 --- a/src/Init/Data/Array/InsertionSort.lean +++ b/src/Init/Data/Array/InsertionSort.lean @@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Basic diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 68a722ed1f..585ad87f87 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Kim Morrison -/ +module + prelude import Init.Data.Nat.Lemmas import Init.Data.List.Range diff --git a/src/Init/Data/Array/Lex.lean b/src/Init/Data/Array/Lex.lean index a700084e4b..4bf9e0f655 100644 --- a/src/Init/Data/Array/Lex.lean +++ b/src/Init/Data/Array/Lex.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Kim Morrison -/ +module + prelude import Init.Data.Array.Lex.Basic import Init.Data.Array.Lex.Lemmas diff --git a/src/Init/Data/Array/Lex/Basic.lean b/src/Init/Data/Array/Lex/Basic.lean index a5b4b978dc..0d287555d7 100644 --- a/src/Init/Data/Array/Lex/Basic.lean +++ b/src/Init/Data/Array/Lex/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Kim Morrison -/ +module + prelude import Init.Data.Array.Basic import Init.Data.Nat.Lemmas diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index 5603ccfd7e..ab56231738 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.List.Lex diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index bb4cbffa8c..2f4162c7f5 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.Array.Attach diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean index d59053472c..b66f520dbd 100644 --- a/src/Init/Data/Array/Mem.lean +++ b/src/Init/Data/Array/Mem.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Joachim Breitner -/ +module + prelude import Init.Data.Array.Basic import Init.Data.Nat.Linear diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean index e647e682d6..4646a209f4 100644 --- a/src/Init/Data/Array/Monadic.lean +++ b/src/Init/Data/Array/Monadic.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.Array.Attach diff --git a/src/Init/Data/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean index d701487f2b..ab6b7532df 100644 --- a/src/Init/Data/Array/OfFn.lean +++ b/src/Init/Data/Array/OfFn.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.List.OfFn diff --git a/src/Init/Data/Array/Perm.lean b/src/Init/Data/Array/Perm.lean index b083784e24..ca23b7ef62 100644 --- a/src/Init/Data/Array/Perm.lean +++ b/src/Init/Data/Array/Perm.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Nat.Perm import Init.Data.Array.Lemmas diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean index 118e66e06b..2c48d71c7a 100644 --- a/src/Init/Data/Array/QSort.lean +++ b/src/Init/Data/Array/QSort.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Vector.Basic import Init.Data.Ord diff --git a/src/Init/Data/Array/Range.lean b/src/Init/Data/Array/Range.lean index 702b935327..c0e332ce0c 100644 --- a/src/Init/Data/Array/Range.lean +++ b/src/Init/Data/Array/Range.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.Array.OfFn diff --git a/src/Init/Data/Array/Set.lean b/src/Init/Data/Array/Set.lean index 5b19bbcbda..8c1c33fc19 100644 --- a/src/Init/Data/Array/Set.lean +++ b/src/Init/Data/Array/Set.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Tactics diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 57cf7eb5cb..a1f8f46b81 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Basic diff --git a/src/Init/Data/Array/Subarray/Split.lean b/src/Init/Data/Array/Subarray/Split.lean index ed973af9d0..f75ae8dd01 100644 --- a/src/Init/Data/Array/Subarray/Split.lean +++ b/src/Init/Data/Array/Subarray/Split.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: David Thrane Christiansen -/ +module + prelude import Init.Data.Array.Basic import Init.Data.Array.Subarray diff --git a/src/Init/Data/Array/TakeDrop.lean b/src/Init/Data/Array/TakeDrop.lean index 8ed803c5e4..7262302a11 100644 --- a/src/Init/Data/Array/TakeDrop.lean +++ b/src/Init/Data/Array/TakeDrop.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.List.Nat.TakeDrop diff --git a/src/Init/Data/Array/Zip.lean b/src/Init/Data/Array/Zip.lean index a199b2e65f..d13d2417bb 100644 --- a/src/Init/Data/Array/Zip.lean +++ b/src/Init/Data/Array/Zip.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.TakeDrop import Init.Data.List.Zip diff --git a/src/Init/Data/BEq.lean b/src/Init/Data/BEq.lean index 3f0282bc31..2cb394352a 100644 --- a/src/Init/Data/BEq.lean +++ b/src/Init/Data/BEq.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Markus Himmel -/ +module + prelude import Init.Data.Bool diff --git a/src/Init/Data/Basic.lean b/src/Init/Data/Basic.lean index ea963f66b3..5a29c6859b 100644 --- a/src/Init/Data/Basic.lean +++ b/src/Init/Data/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Basic import Init.Data.Fin.Basic diff --git a/src/Init/Data/BitVec.lean b/src/Init/Data/BitVec.lean index 3827c1e54e..eef90d4e28 100644 --- a/src/Init/Data/BitVec.lean +++ b/src/Init/Data/BitVec.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.BitVec.Basic import Init.Data.BitVec.Bitblast diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index c8f5216274..10ccee9db0 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed, Siddharth Bhat -/ +module + prelude import Init.Data.Fin.Basic import Init.Data.Nat.Bitwise.Lemmas diff --git a/src/Init/Data/BitVec/BasicAux.lean b/src/Init/Data/BitVec/BasicAux.lean index 4d36d1fdeb..06d331b586 100644 --- a/src/Init/Data/BitVec/BasicAux.lean +++ b/src/Init/Data/BitVec/BasicAux.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed -/ +module + prelude import Init.Data.Fin.Basic diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 7c887c2a9f..5d73b709ff 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat -/ +module + prelude import Init.Data.BitVec.Folds import Init.Data.Nat.Mod diff --git a/src/Init/Data/BitVec/Folds.lean b/src/Init/Data/BitVec/Folds.lean index 3e8a761b87..7ec6050ed3 100644 --- a/src/Init/Data/BitVec/Folds.lean +++ b/src/Init/Data/BitVec/Folds.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joe Hendrix, Harun Khan -/ +module + prelude import Init.Data.BitVec.Lemmas import Init.Data.Nat.Lemmas diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index c383a2bee3..5be70c9e4f 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth Bhat -/ +module + prelude import Init.Data.Bool import Init.Data.BitVec.Basic diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index d5d501b1c6..a8edd526db 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 F. G. Dorais. No rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: F. G. Dorais -/ +module + prelude import Init.NotationExtra diff --git a/src/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean index b6ee6ccf4b..2e513d63f4 100644 --- a/src/Init/Data/ByteArray.lean +++ b/src/Init/Data/ByteArray.lean @@ -3,5 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.ByteArray.Basic diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 6eb545a613..df1425eafa 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Basic import Init.Data.Array.Subarray diff --git a/src/Init/Data/Cast.lean b/src/Init/Data/Cast.lean index 3931fa9fb5..65931ce137 100644 --- a/src/Init/Data/Cast.lean +++ b/src/Init/Data/Cast.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Gabriel Ebner -/ +module + prelude import Init.Coe diff --git a/src/Init/Data/Char.lean b/src/Init/Data/Char.lean index e2476e6b51..8b890f93e8 100644 --- a/src/Init/Data/Char.lean +++ b/src/Init/Data/Char.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Char.Basic import Init.Data.Char.Lemmas diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean index e73f71e4bd..88df42e589 100644 --- a/src/Init/Data/Char/Basic.lean +++ b/src/Init/Data/Char/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.UInt.BasicAux diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean index 3d57fc3a61..4fbc4f43ab 100644 --- a/src/Init/Data/Char/Lemmas.lean +++ b/src/Init/Data/Char/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Char.Basic import Init.Data.UInt.Lemmas diff --git a/src/Init/Data/Fin.lean b/src/Init/Data/Fin.lean index 3b5a8ecc71..172db74a4a 100644 --- a/src/Init/Data/Fin.lean +++ b/src/Init/Data/Fin.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Fin.Basic import Init.Data.Fin.Log2 diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index e0c478a508..1a544ffe12 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro -/ +module + prelude import Init.Data.Nat.Bitwise.Basic diff --git a/src/Init/Data/Fin/Bitwise.lean b/src/Init/Data/Fin/Bitwise.lean index ab1181c6fa..25c582a5f7 100644 --- a/src/Init/Data/Fin/Bitwise.lean +++ b/src/Init/Data/Fin/Bitwise.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ +module + prelude import Init.Data.Nat.Bitwise import Init.Data.Fin.Basic diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index 7d71feaca7..4d4ccd83d2 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 François G. Dorais. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: François G. Dorais -/ +module + prelude import Init.Data.Nat.Linear import Init.Control.Lawful.Basic diff --git a/src/Init/Data/Fin/Iterate.lean b/src/Init/Data/Fin/Iterate.lean index 6d55e44393..880042b9bf 100644 --- a/src/Init/Data/Fin/Iterate.lean +++ b/src/Init/Data/Fin/Iterate.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joe Hendrix -/ +module + prelude import Init.PropLemmas import Init.Data.Fin.Basic diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 6c2a44216d..ceac5a0802 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Leonardo de Moura -/ +module + prelude import Init.Data.Fin.Basic import Init.Data.Nat.Lemmas diff --git a/src/Init/Data/Fin/Log2.lean b/src/Init/Data/Fin/Log2.lean index d3f19d3635..f1cf1aea5c 100644 --- a/src/Init/Data/Fin/Log2.lean +++ b/src/Init/Data/Fin/Log2.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Henrik Böving. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +module + prelude import Init.Data.Nat.Log2 diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index 74350a4f0f..f0331b7504 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Core import Init.Data.Int.Basic diff --git a/src/Init/Data/Float32.lean b/src/Init/Data/Float32.lean index 092d1e1219..1ad084e52c 100644 --- a/src/Init/Data/Float32.lean +++ b/src/Init/Data/Float32.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Core import Init.Data.Int.Basic diff --git a/src/Init/Data/FloatArray.lean b/src/Init/Data/FloatArray.lean index 7c798deaa3..db5f314148 100644 --- a/src/Init/Data/FloatArray.lean +++ b/src/Init/Data/FloatArray.lean @@ -3,5 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.FloatArray.Basic diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean index 4d7dfbdac1..fb416d0f94 100644 --- a/src/Init/Data/FloatArray/Basic.lean +++ b/src/Init/Data/FloatArray/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Basic import Init.Data.Float diff --git a/src/Init/Data/Format.lean b/src/Init/Data/Format.lean index d65e4d4159..a64639991c 100644 --- a/src/Init/Data/Format.lean +++ b/src/Init/Data/Format.lean @@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Format.Basic import Init.Data.Format.Macro diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index 7159e21462..c2c981c16f 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Control.State import Init.Data.Int.Basic diff --git a/src/Init/Data/Format/Instances.lean b/src/Init/Data/Format/Instances.lean index 8d50e8a56b..1df47e08a6 100644 --- a/src/Init/Data/Format/Instances.lean +++ b/src/Init/Data/Format/Instances.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Format.Basic import Init.Data.Array.Basic diff --git a/src/Init/Data/Format/Macro.lean b/src/Init/Data/Format/Macro.lean index b69fed4d64..85e42a603e 100644 --- a/src/Init/Data/Format/Macro.lean +++ b/src/Init/Data/Format/Macro.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Format.Basic import Init.Data.ToString.Macro diff --git a/src/Init/Data/Format/Syntax.lean b/src/Init/Data/Format/Syntax.lean index b876b030d5..4f659ee038 100644 --- a/src/Init/Data/Format/Syntax.lean +++ b/src/Init/Data/Format/Syntax.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Format.Macro import Init.Data.Format.Instances diff --git a/src/Init/Data/Function.lean b/src/Init/Data/Function.lean index c32291205d..6db6c5212d 100644 --- a/src/Init/Data/Function.lean +++ b/src/Init/Data/Function.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Core diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean index 6594537955..a076287fc5 100644 --- a/src/Init/Data/Hashable.lean +++ b/src/Init/Data/Hashable.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.UInt.Basic import Init.Data.String diff --git a/src/Init/Data/Int.lean b/src/Init/Data/Int.lean index 95c2d6c73c..82b7eff9b9 100644 --- a/src/Init/Data/Int.lean +++ b/src/Init/Data/Int.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Int.Basic import Init.Data.Int.Bitwise diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 3b8fe0b595..d79b7fe550 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -5,6 +5,8 @@ Authors: Jeremy Avigad, Leonardo de Moura The integers, with addition, multiplication, and subtraction. -/ +module + prelude import Init.Data.Cast import Init.Data.Nat.Div.Basic diff --git a/src/Init/Data/Int/Bitwise.lean b/src/Init/Data/Int/Bitwise.lean index 61fb1c297e..38623eb7cb 100644 --- a/src/Init/Data/Int/Bitwise.lean +++ b/src/Init/Data/Int/Bitwise.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Int.Bitwise.Basic import Init.Data.Int.Bitwise.Lemmas diff --git a/src/Init/Data/Int/Bitwise/Basic.lean b/src/Init/Data/Int/Bitwise/Basic.lean index 64206c2f69..df0cc71cdf 100644 --- a/src/Init/Data/Int/Bitwise/Basic.lean +++ b/src/Init/Data/Int/Bitwise/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + prelude import Init.Data.Int.Basic import Init.Data.Nat.Bitwise.Basic diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index e25275a7c8..e057d40d77 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Siddharth Bhat. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Siddharth Bhat, Jeremy Avigad -/ +module + prelude import Init.Data.Nat.Bitwise.Lemmas import Init.Data.Int.Bitwise.Basic diff --git a/src/Init/Data/Int/Compare.lean b/src/Init/Data/Int/Compare.lean index e02093737f..8b503c69e7 100644 --- a/src/Init/Data/Int/Compare.lean +++ b/src/Init/Data/Int/Compare.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert -/ +module + prelude import Init.Data.Ord import Init.Data.Int.Order diff --git a/src/Init/Data/Int/Cooper.lean b/src/Init/Data/Int/Cooper.lean index 7963809c05..4afc3286f6 100644 --- a/src/Init/Data/Int/Cooper.lean +++ b/src/Init/Data/Int/Cooper.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Int.DivMod.Lemmas import Init.Data.Int.Gcd diff --git a/src/Init/Data/Int/DivMod.lean b/src/Init/Data/Int/DivMod.lean index c6a7b21ca7..e095ae7579 100644 --- a/src/Init/Data/Int/DivMod.lean +++ b/src/Init/Data/Int/DivMod.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Int.DivMod.Basic import Init.Data.Int.DivMod.Bootstrap diff --git a/src/Init/Data/Int/DivMod/Basic.lean b/src/Init/Data/Int/DivMod/Basic.lean index ff71dfd563..e7e1de68d8 100644 --- a/src/Init/Data/Int/DivMod/Basic.lean +++ b/src/Init/Data/Int/DivMod/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Mario Carneiro -/ +module + prelude import Init.Data.Int.Basic diff --git a/src/Init/Data/Int/DivMod/Bootstrap.lean b/src/Init/Data/Int/DivMod/Bootstrap.lean index 8fcec2d707..6cade6b73a 100644 --- a/src/Init/Data/Int/DivMod/Bootstrap.lean +++ b/src/Init/Data/Int/DivMod/Bootstrap.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Mario Carneiro -/ +module + prelude import Init.Data.Int.DivMod.Basic import Init.Data.Int.Order diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean index 5b780239fe..1e820e9c43 100644 --- a/src/Init/Data/Int/DivMod/Lemmas.lean +++ b/src/Init/Data/Int/DivMod/Lemmas.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Mario Carneiro, Kim Morrison, Markus Himmel -/ +module + prelude import Init.Data.Int.DivMod.Bootstrap import Init.Data.Nat.Lemmas diff --git a/src/Init/Data/Int/Gcd.lean b/src/Init/Data/Int/Gcd.lean index a2d6f226e3..fa536853ab 100644 --- a/src/Init/Data/Int/Gcd.lean +++ b/src/Init/Data/Int/Gcd.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Markus Himmel -/ +module + prelude import Init.Data.Int.Basic import Init.Data.Nat.Gcd diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean index a8306c4739..e3b75a5962 100644 --- a/src/Init/Data/Int/Lemmas.lean +++ b/src/Init/Data/Int/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.Int.Basic import Init.Conv diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 12fe179bb3..0746e90bcf 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Int.Order import Init.Data.Int.Pow diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index 2e0d54feb2..b69e844cad 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/src/Init/Data/Int/Linear.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.ByCases import Init.Data.Prod diff --git a/src/Init/Data/Int/OfNat.lean b/src/Init/Data/Int/OfNat.lean index 58f716dde6..fee57a5f0b 100644 --- a/src/Init/Data/Int/OfNat.lean +++ b/src/Init/Data/Int/OfNat.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Int.Lemmas import Init.Data.Int.DivMod diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean index 59fd94f064..baae77bfa6 100644 --- a/src/Init/Data/Int/Order.lean +++ b/src/Init/Data/Int/Order.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.Int.Lemmas import Init.ByCases diff --git a/src/Init/Data/Int/Pow.lean b/src/Init/Data/Int/Pow.lean index 0b2f3aa699..170784ffe5 100644 --- a/src/Init/Data/Int/Pow.lean +++ b/src/Init/Data/Int/Pow.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.Int.Lemmas import Init.Data.Nat.Lemmas diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean index 6c0cb85bd6..81be021a26 100644 --- a/src/Init/Data/List.lean +++ b/src/Init/Data/List.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.List.Attach import Init.Data.List.Basic diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 45cd28a76c..b6bf8565ee 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + prelude import Init.Data.List.Count import Init.Data.Subtype diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 8755d11cbf..198d02bfb3 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.SimpLemmas import Init.Data.Nat.Basic diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index 834b4379a1..da44feb2d7 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Linear diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 7a69c675ad..03289e0c8d 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Control.Basic import Init.Control.Id diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index b531be23c9..23d4e7a89f 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Sublist diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean index 12d0f64439..11343c90f5 100644 --- a/src/Init/Data/List/Erase.lean +++ b/src/Init/Data/List/Erase.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, Yury Kudryashov -/ +module + prelude import Init.Data.List.Pairwise import Init.Data.List.Find diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean index 818501e0fb..26c86cd67a 100644 --- a/src/Init/Data/List/FinRange.lean +++ b/src/Init/Data/List/FinRange.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 François G. Dorais. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: François G. Dorais -/ +module + prelude import Init.Data.List.OfFn diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 8375154980..0a5f0cad8f 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, Kim Morrison, Jannis Limperg -/ +module + prelude import Init.Data.List.Lemmas import Init.Data.List.Sublist diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index 4b2a120830..82d323f12f 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Array.Bootstrap diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index a3489dd7b5..9200028518 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, Kim Morrison -/ +module + prelude import Init.Data.Bool import Init.Data.Option.Lemmas diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean index e05e0d854a..e27b034560 100644 --- a/src/Init/Data/List/Lex.lean +++ b/src/Init/Data/List/Lex.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Lemmas import Init.Data.List.Nat.TakeDrop diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index 687b1771f2..79a600cbb2 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison, Mario Carneiro -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.List.Nat.Range diff --git a/src/Init/Data/List/MinMax.lean b/src/Init/Data/List/MinMax.lean index 0a9ceb72d1..f9ef30dd06 100644 --- a/src/Init/Data/List/MinMax.lean +++ b/src/Init/Data/List/MinMax.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Lemmas import Init.Data.List.Pairwise diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean index 6f0057fe59..ce1b593fc1 100644 --- a/src/Init/Data/List/Monadic.lean +++ b/src/Init/Data/List/Monadic.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.TakeDrop import Init.Data.List.Attach diff --git a/src/Init/Data/List/Nat.lean b/src/Init/Data/List/Nat.lean index dae9a70f7e..4806c9804a 100644 --- a/src/Init/Data/List/Nat.lean +++ b/src/Init/Data/List/Nat.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Nat.Basic import Init.Data.List.Nat.Pairwise diff --git a/src/Init/Data/List/Nat/BEq.lean b/src/Init/Data/List/Nat/BEq.lean index fd8f61f6a4..fbb503df8c 100644 --- a/src/Init/Data/List/Nat/BEq.lean +++ b/src/Init/Data/List/Nat/BEq.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Nat.Lemmas import Init.Data.List.Basic diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index 9fcc8c6ad4..8d9ef44ba6 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Count import Init.Data.List.Find diff --git a/src/Init/Data/List/Nat/Count.lean b/src/Init/Data/List/Nat/Count.lean index 0d2e3aba21..1c31218213 100644 --- a/src/Init/Data/List/Nat/Count.lean +++ b/src/Init/Data/List/Nat/Count.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Kim Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Count import Init.Data.Nat.Lemmas diff --git a/src/Init/Data/List/Nat/Erase.lean b/src/Init/Data/List/Nat/Erase.lean index 6f1c561d7f..1d0c347914 100644 --- a/src/Init/Data/List/Nat/Erase.lean +++ b/src/Init/Data/List/Nat/Erase.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Kim Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Nat.TakeDrop import Init.Data.List.Erase diff --git a/src/Init/Data/List/Nat/Find.lean b/src/Init/Data/List/Nat/Find.lean index 1363268832..e63728baf0 100644 --- a/src/Init/Data/List/Nat/Find.lean +++ b/src/Init/Data/List/Nat/Find.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Kim Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Nat.Range import Init.Data.List.Find diff --git a/src/Init/Data/List/Nat/InsertIdx.lean b/src/Init/Data/List/Nat/InsertIdx.lean index af2bf07c05..fd508f4a46 100644 --- a/src/Init/Data/List/Nat/InsertIdx.lean +++ b/src/Init/Data/List/Nat/InsertIdx.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Nat.Modify diff --git a/src/Init/Data/List/Nat/Modify.lean b/src/Init/Data/List/Nat/Modify.lean index c822cdcff0..2d9523c492 100644 --- a/src/Init/Data/List/Nat/Modify.lean +++ b/src/Init/Data/List/Nat/Modify.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Nat.TakeDrop import Init.Data.List.Nat.Erase diff --git a/src/Init/Data/List/Nat/Pairwise.lean b/src/Init/Data/List/Nat/Pairwise.lean index e7020b33a9..3da319cebd 100644 --- a/src/Init/Data/List/Nat/Pairwise.lean +++ b/src/Init/Data/List/Nat/Pairwise.lean @@ -3,6 +3,8 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, James Gallicchio -/ +module + prelude import Init.Data.Fin.Lemmas import Init.Data.List.Nat.TakeDrop diff --git a/src/Init/Data/List/Nat/Perm.lean b/src/Init/Data/List/Nat/Perm.lean index 8c5b907a49..61d106f62a 100644 --- a/src/Init/Data/List/Nat/Perm.lean +++ b/src/Init/Data/List/Nat/Perm.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Nat.TakeDrop import Init.Data.List.Perm diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean index 3bc53e7824..8664435f2d 100644 --- a/src/Init/Data/List/Nat/Range.lean +++ b/src/Init/Data/List/Nat/Range.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Nat.TakeDrop import Init.Data.List.Range diff --git a/src/Init/Data/List/Nat/Sublist.lean b/src/Init/Data/List/Nat/Sublist.lean index 944f27cea7..1d53944a42 100644 --- a/src/Init/Data/List/Nat/Sublist.lean +++ b/src/Init/Data/List/Nat/Sublist.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Sublist import Init.Data.List.Nat.Basic diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index c97dc112ab..d601d40e19 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Zip import Init.Data.List.Sublist diff --git a/src/Init/Data/List/Notation.lean b/src/Init/Data/List/Notation.lean index a213a220a3..9d3380ac23 100644 --- a/src/Init/Data/List/Notation.lean +++ b/src/Init/Data/List/Notation.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Div.Basic diff --git a/src/Init/Data/List/OfFn.lean b/src/Init/Data/List/OfFn.lean index 580fb21c66..4a1af6073d 100644 --- a/src/Init/Data/List/OfFn.lean +++ b/src/Init/Data/List/OfFn.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Kim Morrison -/ +module + prelude import Init.Data.List.Basic import Init.Data.Fin.Fold diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean index c9a6875685..b804eaca49 100644 --- a/src/Init/Data/List/Pairwise.lean +++ b/src/Init/Data/List/Pairwise.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Sublist import Init.Data.List.Attach diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean index 3625bcb1d9..dc481f6eab 100644 --- a/src/Init/Data/List/Perm.lean +++ b/src/Init/Data/List/Perm.lean @@ -3,6 +3,8 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ +module + prelude import Init.Data.List.Pairwise import Init.Data.List.Erase diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean index 28e3fce0fc..ef07468b8e 100644 --- a/src/Init/Data/List/Range.lean +++ b/src/Init/Data/List/Range.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Pairwise import Init.Data.List.Zip diff --git a/src/Init/Data/List/Sort.lean b/src/Init/Data/List/Sort.lean index d26785c28d..887f40ac41 100644 --- a/src/Init/Data/List/Sort.lean +++ b/src/Init/Data/List/Sort.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Sort.Basic import Init.Data.List.Sort.Impl diff --git a/src/Init/Data/List/Sort/Basic.lean b/src/Init/Data/List/Sort/Basic.lean index 2538f39d7c..db7982a934 100644 --- a/src/Init/Data/List/Sort/Basic.lean +++ b/src/Init/Data/List/Sort/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Impl import Init.Data.List.Nat.TakeDrop diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean index d20177127c..d916ca16f0 100644 --- a/src/Init/Data/List/Sort/Impl.lean +++ b/src/Init/Data/List/Sort/Impl.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Sort.Lemmas diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index 4c85aae7aa..0c8d137588 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison, Eric Wieser, François G. Dorais -/ +module + prelude import Init.Data.List.Perm import Init.Data.List.Sort.Basic diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 327f4d8441..e640c64e7d 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, Kim Morrison -/ +module + prelude import Init.Data.List.TakeDrop diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index ce1077b2d2..3ca3d90869 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.Lemmas diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 192bfe7c79..68b5ee671a 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + prelude import Init.Data.List.Impl import Init.Data.List.Nat.Erase diff --git a/src/Init/Data/List/ToArrayImpl.lean b/src/Init/Data/List/ToArrayImpl.lean index 926b13c711..1611ad9fc5 100644 --- a/src/Init/Data/List/ToArrayImpl.lean +++ b/src/Init/Data/List/ToArrayImpl.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +module + prelude import Init.Data.List.Basic diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index 883ead986d..55e91b3223 100644 --- a/src/Init/Data/List/Zip.lean +++ b/src/Init/Data/List/Zip.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +module + prelude import Init.Data.List.TakeDrop import Init.Data.Function diff --git a/src/Init/Data/Nat.lean b/src/Init/Data/Nat.lean index a37fee411d..0b7181f819 100644 --- a/src/Init/Data/Nat.lean +++ b/src/Init/Data/Nat.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Basic import Init.Data.Nat.Div.Basic diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 77e80cb9c4..cb1e3b991b 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Leonardo de Moura -/ +module + prelude import Init.SimpLemmas import Init.Data.NeZero diff --git a/src/Init/Data/Nat/Bitwise.lean b/src/Init/Data/Nat/Bitwise.lean index 9a4a845d74..1988c1d6a3 100644 --- a/src/Init/Data/Nat/Bitwise.lean +++ b/src/Init/Data/Nat/Bitwise.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Nat.Bitwise.Basic import Init.Data.Nat.Bitwise.Lemmas diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index 1dead23820..879bef0bdd 100644 --- a/src/Init/Data/Nat/Bitwise/Basic.lean +++ b/src/Init/Data/Nat/Bitwise/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Basic import Init.Data.Nat.Div.Basic diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index 88e4ae21a5..b33f9ef665 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joe Hendrix -/ +module + prelude import Init.Data.Bool import Init.Data.Int.Pow diff --git a/src/Init/Data/Nat/Compare.lean b/src/Init/Data/Nat/Compare.lean index 3736ae9ab5..d72b8d5879 100644 --- a/src/Init/Data/Nat/Compare.lean +++ b/src/Init/Data/Nat/Compare.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ +module + prelude import Init.Data.Ord diff --git a/src/Init/Data/Nat/Control.lean b/src/Init/Data/Nat/Control.lean index 187b78e9d7..ad482c21e4 100644 --- a/src/Init/Data/Nat/Control.lean +++ b/src/Init/Data/Nat/Control.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Control.Basic import Init.Data.Nat.Basic diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index a7b22d338d..6673422d9f 100644 --- a/src/Init/Data/Nat/Div.lean +++ b/src/Init/Data/Nat/Div.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Nat.Div.Basic import Init.Data.Nat.Div.Lemmas diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean index 69b7b5e155..234f26532d 100644 --- a/src/Init/Data/Nat/Div/Basic.lean +++ b/src/Init/Data/Nat/Div/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.WF import Init.WFTactics diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean index 219b8c5799..b0fe7f8289 100644 --- a/src/Init/Data/Nat/Div/Lemmas.lean +++ b/src/Init/Data/Nat/Div/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Omega import Init.Data.Nat.Lemmas diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean index 60b6e66618..33e701c03e 100644 --- a/src/Init/Data/Nat/Dvd.lean +++ b/src/Init/Data/Nat/Dvd.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ +module + prelude import Init.Data.Nat.Div.Basic import Init.Meta diff --git a/src/Init/Data/Nat/Fold.lean b/src/Init/Data/Nat/Fold.lean index 018aa4dfe5..f1dd702ec7 100644 --- a/src/Init/Data/Nat/Fold.lean +++ b/src/Init/Data/Nat/Fold.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Leonardo de Moura, Kim Morrison -/ +module + prelude import Init.Omega import Init.Data.List.FinRange diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean index d7599e86f9..9df502ff49 100644 --- a/src/Init/Data/Nat/Gcd.lean +++ b/src/Init/Data/Nat/Gcd.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Markus Himmel -/ +module + prelude import Init.Data.Nat.Dvd import Init.NotationExtra diff --git a/src/Init/Data/Nat/Lcm.lean b/src/Init/Data/Nat/Lcm.lean index 355a931d2e..56b00156d4 100644 --- a/src/Init/Data/Nat/Lcm.lean +++ b/src/Init/Data/Nat/Lcm.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Markus Himmel -/ +module + prelude import Init.Data.Nat.Gcd import Init.Data.Nat.Lemmas diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 725d890c64..aca0ee5510 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights r Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Floris van Doorn -/ +module + prelude import Init.Data.Nat.MinMax import Init.Data.Nat.Log2 diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean index 6a0477379c..0771c84227 100644 --- a/src/Init/Data/Nat/Linear.lean +++ b/src/Init/Data/Nat/Linear.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.ByCases import Init.Data.Prod diff --git a/src/Init/Data/Nat/Log2.lean b/src/Init/Data/Nat/Log2.lean index 6bf217e3b3..5497e7d99c 100644 --- a/src/Init/Data/Nat/Log2.lean +++ b/src/Init/Data/Nat/Log2.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ +module + prelude import Init.Data.Nat.Linear diff --git a/src/Init/Data/Nat/MinMax.lean b/src/Init/Data/Nat/MinMax.lean index 608520fd93..f682da0faa 100644 --- a/src/Init/Data/Nat/MinMax.lean +++ b/src/Init/Data/Nat/MinMax.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ +module + prelude import Init.ByCases diff --git a/src/Init/Data/Nat/Mod.lean b/src/Init/Data/Nat/Mod.lean index 87fdd7b0e5..d33d5102d0 100644 --- a/src/Init/Data/Nat/Mod.lean +++ b/src/Init/Data/Nat/Mod.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Omega diff --git a/src/Init/Data/Nat/Power2.lean b/src/Init/Data/Nat/Power2.lean index c9b9f85839..a76d7645ca 100644 --- a/src/Init/Data/Nat/Power2.lean +++ b/src/Init/Data/Nat/Power2.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Linear diff --git a/src/Init/Data/Nat/SOM.lean b/src/Init/Data/Nat/SOM.lean index f021500d88..8d5cedd86e 100644 --- a/src/Init/Data/Nat/SOM.lean +++ b/src/Init/Data/Nat/SOM.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Linear import Init.Data.List.BasicAux diff --git a/src/Init/Data/Nat/Simproc.lean b/src/Init/Data/Nat/Simproc.lean index 285937978b..1e5a6ff96c 100644 --- a/src/Init/Data/Nat/Simproc.lean +++ b/src/Init/Data/Nat/Simproc.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joe Hendrix -/ +module + prelude import Init.Data.Bool import Init.Data.Nat.Basic diff --git a/src/Init/Data/NeZero.lean b/src/Init/Data/NeZero.lean index 6cebc7bc4b..f424210ced 100644 --- a/src/Init/Data/NeZero.lean +++ b/src/Init/Data/NeZero.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Eric Rodriguez. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Rodriguez -/ +module + prelude import Init.Data.Zero diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean index 4c044c876e..7b88f40427 100644 --- a/src/Init/Data/OfScientific.lean +++ b/src/Init/Data/OfScientific.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Meta import Init.Data.Float diff --git a/src/Init/Data/Option.lean b/src/Init/Data/Option.lean index cfd5554c13..7e999aa784 100644 --- a/src/Init/Data/Option.lean +++ b/src/Init/Data/Option.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Option.Basic import Init.Data.Option.BasicAux diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean index e2682c62f6..e06f71f461 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Option.Basic import Init.Data.Option.List diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index 2634b82139..f32822aef2 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Control.Basic diff --git a/src/Init/Data/Option/BasicAux.lean b/src/Init/Data/Option/BasicAux.lean index 770da08e1e..b52c6defe2 100644 --- a/src/Init/Data/Option/BasicAux.lean +++ b/src/Init/Data/Option/BasicAux.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Option.Basic import Init.Util diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean index 88bdbc4779..eb2ec3fcdd 100644 --- a/src/Init/Data/Option/Instances.lean +++ b/src/Init/Data/Option/Instances.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Option.Basic diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index 9087983f66..75ba37f999 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + prelude import Init.Data.Option.BasicAux import Init.Data.Option.Instances diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean index 93c876b606..23989ab347 100644 --- a/src/Init/Data/Option/List.lean +++ b/src/Init/Data/Option/List.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Lemmas diff --git a/src/Init/Data/Option/Monadic.lean b/src/Init/Data/Option/Monadic.lean index c190c001c9..32e36e11e4 100644 --- a/src/Init/Data/Option/Monadic.lean +++ b/src/Init/Data/Option/Monadic.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Option.Attach diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean index 974af4717f..1cc13e687f 100644 --- a/src/Init/Data/Ord.lean +++ b/src/Init/Data/Ord.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Dany Fabian, Sebastian Ullrich -/ +module + prelude import Init.Data.String import Init.Data.Array.Basic diff --git a/src/Init/Data/PLift.lean b/src/Init/Data/PLift.lean index d03ab7ccda..e57df0e20d 100644 --- a/src/Init/Data/PLift.lean +++ b/src/Init/Data/PLift.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Core diff --git a/src/Init/Data/Prod.lean b/src/Init/Data/Prod.lean index b2477c7731..10b2120b37 100644 --- a/src/Init/Data/Prod.lean +++ b/src/Init/Data/Prod.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.SimpLemmas import Init.NotationExtra diff --git a/src/Init/Data/Queue.lean b/src/Init/Data/Queue.lean index 8439425d91..70d752e9f9 100644 --- a/src/Init/Data/Queue.lean +++ b/src/Init/Data/Queue.lean @@ -6,6 +6,8 @@ Authors: Daniel Selsam Simple queue implemented using two lists. Note: this is only a temporary placeholder. -/ +module + prelude import Init.Data.Array.Basic diff --git a/src/Init/Data/RArray.lean b/src/Init/Data/RArray.lean index 0b423d8fdd..9df883e6ac 100644 --- a/src/Init/Data/RArray.lean +++ b/src/Init/Data/RArray.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ +module + prelude import Init.PropLemmas diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index 2bdacf84d9..c4b1bf80b3 100644 --- a/src/Init/Data/Random.lean +++ b/src/Init/Data/Random.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.System.IO universe u diff --git a/src/Init/Data/Range.lean b/src/Init/Data/Range.lean index 1915f4be9b..22fe810b61 100644 --- a/src/Init/Data/Range.lean +++ b/src/Init/Data/Range.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Range.Basic import Init.Data.Range.Lemmas diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean index 0fa732dabc..41c7678c0e 100644 --- a/src/Init/Data/Range/Basic.lean +++ b/src/Init/Data/Range/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Meta import Init.Omega diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean index 63eaa573bd..cb81db818a 100644 --- a/src/Init/Data/Range/Lemmas.lean +++ b/src/Init/Data/Range/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Range.Basic import Init.Data.List.Range diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index 6235eb1638..ad6e5b22b1 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Format.Basic open Sum Subtype Nat diff --git a/src/Init/Data/SInt.lean b/src/Init/Data/SInt.lean index b961a8f299..dcb8d0da8b 100644 --- a/src/Init/Data/SInt.lean +++ b/src/Init/Data/SInt.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +module + prelude import Init.Data.SInt.Basic import Init.Data.SInt.Float diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean index f2f58923c3..45544bb839 100644 --- a/src/Init/Data/SInt/Basic.lean +++ b/src/Init/Data/SInt/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +module + prelude import Init.Data.UInt.Basic diff --git a/src/Init/Data/SInt/Bitwise.lean b/src/Init/Data/SInt/Bitwise.lean index 63557edf59..b45b56dc95 100644 --- a/src/Init/Data/SInt/Bitwise.lean +++ b/src/Init/Data/SInt/Bitwise.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ +module + prelude import Init.Data.UInt.Bitwise import Init.Data.SInt.Lemmas diff --git a/src/Init/Data/SInt/Float.lean b/src/Init/Data/SInt/Float.lean index 08f06c0924..069270854e 100644 --- a/src/Init/Data/SInt/Float.lean +++ b/src/Init/Data/SInt/Float.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ +module + prelude import Init.Data.Float import Init.Data.SInt.Basic diff --git a/src/Init/Data/SInt/Float32.lean b/src/Init/Data/SInt/Float32.lean index 1161a1f17c..d73fb7dd4a 100644 --- a/src/Init/Data/SInt/Float32.lean +++ b/src/Init/Data/SInt/Float32.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ +module + prelude import Init.Data.Float32 import Init.Data.SInt.Basic diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean index d46c879115..ffe040a0a9 100644 --- a/src/Init/Data/SInt/Lemmas.lean +++ b/src/Init/Data/SInt/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ +module + prelude import Init.Data.SInt.Basic import Init.Data.BitVec.Bitblast diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean index 7ff4e6d4a2..843d9007a5 100644 --- a/src/Init/Data/Stream.lean +++ b/src/Init/Data/Stream.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich, Andrew Kent, Leonardo de Moura -/ +module + prelude import Init.Data.Array.Subarray import Init.Data.Range diff --git a/src/Init/Data/String.lean b/src/Init/Data/String.lean index 7232ac73f9..462539a0e4 100644 --- a/src/Init/Data/String.lean +++ b/src/Init/Data/String.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.String.Basic import Init.Data.String.Extra diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index ac8a690020..ece68b6009 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Data.List.Basic import Init.Data.Char.Basic diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index 29c2ac8fd1..1a3a2ec6b6 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.ByteArray import Init.Data.UInt.Lemmas diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean index ddbeface63..45371af529 100644 --- a/src/Init/Data/String/Lemmas.lean +++ b/src/Init/Data/String/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Char.Lemmas import Init.Data.List.Lex diff --git a/src/Init/Data/Subtype.lean b/src/Init/Data/Subtype.lean index 5102dc9348..486b2f33a0 100644 --- a/src/Init/Data/Subtype.lean +++ b/src/Init/Data/Subtype.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl -/ +module + prelude import Init.Ext import Init.Core diff --git a/src/Init/Data/Sum.lean b/src/Init/Data/Sum.lean index d2440d8c28..69807be6d3 100644 --- a/src/Init/Data/Sum.lean +++ b/src/Init/Data/Sum.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Yury G. Kudryashov -/ +module + prelude import Init.Data.Sum.Basic import Init.Data.Sum.Lemmas diff --git a/src/Init/Data/Sum/Basic.lean b/src/Init/Data/Sum/Basic.lean index 4eeb3bf5b7..a66aad79a4 100644 --- a/src/Init/Data/Sum/Basic.lean +++ b/src/Init/Data/Sum/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Yury G. Kudryashov -/ +module + prelude import Init.PropLemmas diff --git a/src/Init/Data/Sum/Lemmas.lean b/src/Init/Data/Sum/Lemmas.lean index 0a316e1207..9235fffebc 100644 --- a/src/Init/Data/Sum/Lemmas.lean +++ b/src/Init/Data/Sum/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Yury G. Kudryashov -/ +module + prelude import Init.Data.Sum.Basic import Init.Ext diff --git a/src/Init/Data/ToString.lean b/src/Init/Data/ToString.lean index e5d7e81c79..09ea314884 100644 --- a/src/Init/Data/ToString.lean +++ b/src/Init/Data/ToString.lean @@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.ToString.Basic import Init.Data.ToString.Macro diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean index 242fac8ee7..605da2a025 100644 --- a/src/Init/Data/ToString/Basic.lean +++ b/src/Init/Data/ToString/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Data.Repr import Init.Data.Option.Basic diff --git a/src/Init/Data/ToString/Macro.lean b/src/Init/Data/ToString/Macro.lean index eb113feaf7..1e8ee44ad4 100644 --- a/src/Init/Data/ToString/Macro.lean +++ b/src/Init/Data/ToString/Macro.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.Meta import Init.Data.ToString.Basic diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean index ed99636dba..0b6c2f9e0c 100644 --- a/src/Init/Data/UInt.lean +++ b/src/Init/Data/UInt.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Henrik Böving. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +module + prelude import Init.Data.UInt.BasicAux import Init.Data.UInt.Basic diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean index 6fbe7271bc..15a0788e4f 100644 --- a/src/Init/Data/UInt/Basic.lean +++ b/src/Init/Data/UInt/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.UInt.BasicAux import Init.Data.BitVec.Basic diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean index 23387bc107..f8096c1cc5 100644 --- a/src/Init/Data/UInt/BasicAux.lean +++ b/src/Init/Data/UInt/BasicAux.lean @@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Fin.Basic import Init.Data.BitVec.BasicAux diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean index d287d3e68c..51562672d1 100644 --- a/src/Init/Data/UInt/Bitwise.lean +++ b/src/Init/Data/UInt/Bitwise.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel, Mac Malone -/ +module + prelude import Init.Data.UInt.Lemmas import Init.Data.Fin.Bitwise diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index 8e759da832..df4057ecb4 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, François G. Dorais, Mario Carneiro, Mac Malone, Markus Himmel -/ +module + prelude import Init.Data.UInt.Basic import Init.Data.Fin.Lemmas diff --git a/src/Init/Data/UInt/Log2.lean b/src/Init/Data/UInt/Log2.lean index f459901ed1..07ed399c18 100644 --- a/src/Init/Data/UInt/Log2.lean +++ b/src/Init/Data/UInt/Log2.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Henrik Böving. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +module + prelude import Init.Data.Fin.Log2 diff --git a/src/Init/Data/ULift.lean b/src/Init/Data/ULift.lean index 91276ebfea..ca26002964 100644 --- a/src/Init/Data/ULift.lean +++ b/src/Init/Data/ULift.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Core diff --git a/src/Init/Data/Vector.lean b/src/Init/Data/Vector.lean index c3cac5f2e6..885e220b76 100644 --- a/src/Init/Data/Vector.lean +++ b/src/Init/Data/Vector.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Basic import Init.Data.Vector.Lemmas diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean index dbca4b2fa0..5bb276fb62 100644 --- a/src/Init/Data/Vector/Attach.lean +++ b/src/Init/Data/Vector/Attach.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Lemmas import Init.Data.Array.Attach diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index cdb17d38bc..af00cd9aff 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Shreyas Srinivas, François G. Dorais, Kim Morrison -/ +module + prelude import Init.Data.Array.Lemmas import Init.Data.Array.MapIdx diff --git a/src/Init/Data/Vector/Count.lean b/src/Init/Data/Vector/Count.lean index 63a666c889..463659343c 100644 --- a/src/Init/Data/Vector/Count.lean +++ b/src/Init/Data/Vector/Count.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Count import Init.Data.Vector.Lemmas diff --git a/src/Init/Data/Vector/DecidableEq.lean b/src/Init/Data/Vector/DecidableEq.lean index b9b2e6c834..8321575139 100644 --- a/src/Init/Data/Vector/DecidableEq.lean +++ b/src/Init/Data/Vector/DecidableEq.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.DecidableEq import Init.Data.Vector.Lemmas diff --git a/src/Init/Data/Vector/Erase.lean b/src/Init/Data/Vector/Erase.lean index 7a6cf3ed61..cd0cfbf1e6 100644 --- a/src/Init/Data/Vector/Erase.lean +++ b/src/Init/Data/Vector/Erase.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Lemmas import Init.Data.Array.Erase diff --git a/src/Init/Data/Vector/Extract.lean b/src/Init/Data/Vector/Extract.lean index b5b7eeef77..b287d7edc7 100644 --- a/src/Init/Data/Vector/Extract.lean +++ b/src/Init/Data/Vector/Extract.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Lemmas import Init.Data.Array.Extract diff --git a/src/Init/Data/Vector/FinRange.lean b/src/Init/Data/Vector/FinRange.lean index af6fc0c740..3b1e3d856a 100644 --- a/src/Init/Data/Vector/FinRange.lean +++ b/src/Init/Data/Vector/FinRange.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 François G. Dorais. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: François G. Dorais -/ +module + prelude import Init.Data.Array.FinRange import Init.Data.Vector.OfFn diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean index a1b376fdb8..9edc2f9219 100644 --- a/src/Init/Data/Vector/Find.lean +++ b/src/Init/Data/Vector/Find.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Lemmas import Init.Data.Vector.Attach diff --git a/src/Init/Data/Vector/InsertIdx.lean b/src/Init/Data/Vector/InsertIdx.lean index 6c59ed960a..ad1a150be0 100644 --- a/src/Init/Data/Vector/InsertIdx.lean +++ b/src/Init/Data/Vector/InsertIdx.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Lemmas import Init.Data.Array.InsertIdx diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index a17f96fa55..972f2cde0b 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Shreyas Srinivas. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison -/ +module + prelude import Init.Data.Vector.Basic import Init.Data.Array.Attach diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index 763328034e..8c6b932e25 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Basic import Init.Data.Vector.Lemmas diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean index e600ebb692..e1971d51af 100644 --- a/src/Init/Data/Vector/MapIdx.lean +++ b/src/Init/Data/Vector/MapIdx.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.MapIdx import Init.Data.Vector.Attach diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index bcff54ee79..f95042d116 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/src/Init/Data/Vector/Monadic.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Lemmas import Init.Data.Vector.Attach diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean index 2f2fa867cb..02bc7cd8df 100644 --- a/src/Init/Data/Vector/OfFn.lean +++ b/src/Init/Data/Vector/OfFn.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Lemmas import Init.Data.Array.OfFn diff --git a/src/Init/Data/Vector/Perm.lean b/src/Init/Data/Vector/Perm.lean index d17c9d519f..beb0592ab2 100644 --- a/src/Init/Data/Vector/Perm.lean +++ b/src/Init/Data/Vector/Perm.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Perm import Init.Data.Vector.Lemmas diff --git a/src/Init/Data/Vector/Range.lean b/src/Init/Data/Vector/Range.lean index dd1e58517e..4bcb49e884 100644 --- a/src/Init/Data/Vector/Range.lean +++ b/src/Init/Data/Vector/Range.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Vector.Lemmas import Init.Data.Vector.Zip diff --git a/src/Init/Data/Vector/Zip.lean b/src/Init/Data/Vector/Zip.lean index 5d0224abd6..023478bd87 100644 --- a/src/Init/Data/Vector/Zip.lean +++ b/src/Init/Data/Vector/Zip.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Array.Zip import Init.Data.Vector.Lemmas diff --git a/src/Init/Data/Zero.lean b/src/Init/Data/Zero.lean index 480167abe3..85a3ccc0b3 100644 --- a/src/Init/Data/Zero.lean +++ b/src/Init/Data/Zero.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Gabriel Ebner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Mario Carneiro -/ +module + prelude import Init.Core diff --git a/src/Init/Dynamic.lean b/src/Init/Dynamic.lean index f80e882808..d02295a105 100644 --- a/src/Init/Dynamic.lean +++ b/src/Init/Dynamic.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ +module + prelude import Init.Core diff --git a/src/Init/Ext.lean b/src/Init/Ext.lean index ad860a15e7..ecf5a71ea7 100644 --- a/src/Init/Ext.lean +++ b/src/Init/Ext.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Gabriel Ebner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Mario Carneiro -/ +module + prelude import Init.Data.ToString.Macro import Init.TacticsExtra diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 55c04fb9b9..52d74536e3 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Util diff --git a/src/Init/Grind.lean b/src/Init/Grind.lean index 2854494150..8d25afee46 100644 --- a/src/Init/Grind.lean +++ b/src/Init/Grind.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Grind.Norm import Init.Grind.Tactics diff --git a/src/Init/Grind/Cases.lean b/src/Init/Grind/Cases.lean index bbe9968ea1..7f34daa9e1 100644 --- a/src/Init/Grind/Cases.lean +++ b/src/Init/Grind/Cases.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Core import Init.Grind.Tactics diff --git a/src/Init/Grind/CommRing.lean b/src/Init/Grind/CommRing.lean index 2c3c675b8a..a7c8f186a3 100644 --- a/src/Init/Grind/CommRing.lean +++ b/src/Init/Grind/CommRing.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Grind.CommRing.Basic import Init.Grind.CommRing.Int diff --git a/src/Init/Grind/CommRing/Basic.lean b/src/Init/Grind/CommRing/Basic.lean index 5440d4c873..f332b4ca78 100644 --- a/src/Init/Grind/CommRing/Basic.lean +++ b/src/Init/Grind/CommRing/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Zero import Init.Data.Int.DivMod.Lemmas diff --git a/src/Init/Grind/CommRing/BitVec.lean b/src/Init/Grind/CommRing/BitVec.lean index 0af5910691..8bb889b953 100644 --- a/src/Init/Grind/CommRing/BitVec.lean +++ b/src/Init/Grind/CommRing/BitVec.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Grind.CommRing.Basic import Init.Data.BitVec.Lemmas diff --git a/src/Init/Grind/CommRing/Int.lean b/src/Init/Grind/CommRing/Int.lean index bc690c2949..71f0c2e835 100644 --- a/src/Init/Grind/CommRing/Int.lean +++ b/src/Init/Grind/CommRing/Int.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Grind.CommRing.Basic import Init.Data.Int.Lemmas diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean index e8d24e8ac6..e945bdfcc6 100644 --- a/src/Init/Grind/CommRing/Poly.lean +++ b/src/Init/Grind/CommRing/Poly.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Lemmas import Init.Data.Hashable diff --git a/src/Init/Grind/CommRing/SInt.lean b/src/Init/Grind/CommRing/SInt.lean index c8d8881450..4ab5cd8ec4 100644 --- a/src/Init/Grind/CommRing/SInt.lean +++ b/src/Init/Grind/CommRing/SInt.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Grind.CommRing.Basic import Init.Data.SInt.Lemmas diff --git a/src/Init/Grind/CommRing/UInt.lean b/src/Init/Grind/CommRing/UInt.lean index 0777e83351..c3c7e0e18f 100644 --- a/src/Init/Grind/CommRing/UInt.lean +++ b/src/Init/Grind/CommRing/UInt.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Grind.CommRing.Basic import Init.Data.UInt.Lemmas diff --git a/src/Init/Grind/Ext.lean b/src/Init/Grind/Ext.lean index 8b52ec06c7..1c2d58af68 100644 --- a/src/Init/Grind/Ext.lean +++ b/src/Init/Grind/Ext.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Ext import Init.Grind.Tactics diff --git a/src/Init/Grind/Lemmas.lean b/src/Init/Grind/Lemmas.lean index 28a309ff39..be709c6318 100644 --- a/src/Init/Grind/Lemmas.lean +++ b/src/Init/Grind/Lemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Core import Init.SimpLemmas diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean index 0d65b237a6..cdf7a513df 100644 --- a/src/Init/Grind/Norm.lean +++ b/src/Init/Grind/Norm.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.SimpLemmas import Init.PropLemmas diff --git a/src/Init/Grind/Offset.lean b/src/Init/Grind/Offset.lean index 0621780ab1..5c311b7a46 100644 --- a/src/Init/Grind/Offset.lean +++ b/src/Init/Grind/Offset.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Core import Init.Omega diff --git a/src/Init/Grind/PP.lean b/src/Init/Grind/PP.lean index 8eb8d3aa85..9e438aa15f 100644 --- a/src/Init/Grind/PP.lean +++ b/src/Init/Grind/PP.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.NotationExtra diff --git a/src/Init/Grind/Propagator.lean b/src/Init/Grind/Propagator.lean index 0edb9d8fb4..ae72a6cef7 100644 --- a/src/Init/Grind/Propagator.lean +++ b/src/Init/Grind/Propagator.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.NotationExtra diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index fc2ae8e2b7..9cff8fa61d 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Tactics diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean index fb17f67a6a..b1688589ea 100644 --- a/src/Init/Grind/Util.lean +++ b/src/Init/Grind/Util.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Core import Init.Classical diff --git a/src/Init/Guard.lean b/src/Init/Guard.lean index 03877c2eb9..6c722439d5 100644 --- a/src/Init/Guard.lean +++ b/src/Init/Guard.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + prelude import Init.Tactics import Init.Conv diff --git a/src/Init/Hints.lean b/src/Init/Hints.lean index e8a2904e63..2d314d7340 100644 --- a/src/Init/Hints.lean +++ b/src/Init/Hints.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.NotationExtra diff --git a/src/Init/Internal.lean b/src/Init/Internal.lean index 2bf2266b69..d4beb95f76 100644 --- a/src/Init/Internal.lean +++ b/src/Init/Internal.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ +module + prelude import Init.Internal.Order diff --git a/src/Init/Internal/Order.lean b/src/Init/Internal/Order.lean index 49eac64248..47e5bda942 100644 --- a/src/Init/Internal/Order.lean +++ b/src/Init/Internal/Order.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ +module + prelude import Init.Internal.Order.Basic import Init.Internal.Order.Lemmas diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index b874a168e1..4bc0fc2fd4 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ +module + prelude import Init.ByCases diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean index 16d45faa01..71b87b462e 100644 --- a/src/Init/Internal/Order/Lemmas.lean +++ b/src/Init/Internal/Order/Lemmas.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ +module + prelude import Init.Data.List.Control diff --git a/src/Init/Internal/Order/Tactic.lean b/src/Init/Internal/Order/Tactic.lean index 574990e877..b90da099a6 100644 --- a/src/Init/Internal/Order/Tactic.lean +++ b/src/Init/Internal/Order/Tactic.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ +module + prelude import Init.Notation diff --git a/src/Init/MacroTrace.lean b/src/Init/MacroTrace.lean index 11ae3290c7..093ff10850 100644 --- a/src/Init/MacroTrace.lean +++ b/src/Init/MacroTrace.lean @@ -6,6 +6,8 @@ Authors: Leonardo de Moura Extra notation that depends on Init/Meta -/ +module + prelude import Init.Data.ToString.Macro import Init.Meta diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index a835895a02..941ce42217 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -5,6 +5,8 @@ Authors: Leonardo de Moura and Sebastian Ullrich Additional goodies for writing macros -/ +module + prelude import Init.MetaTypes import Init.Syntax diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index ef39aa56b3..1bdbc15b42 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -3,6 +3,8 @@ Copyright (c) Leonardo de Moura. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Core diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 1d3d27702e..d0b705849e 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Mario Carneiro Notation for operators defined at Prelude.lean -/ +module + prelude import Init.Prelude import Init.Coe diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index e44ba0930e..3df120dbe9 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -5,6 +5,8 @@ Authors: Leonardo de Moura Extra notation that depends on Init/Meta -/ +module + prelude import Init.Data.ToString.Basic import Init.Data.Array.Subarray diff --git a/src/Init/Omega.lean b/src/Init/Omega.lean index 4d501a70c7..786e95e347 100644 --- a/src/Init/Omega.lean +++ b/src/Init/Omega.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Omega.Int import Init.Omega.IntList diff --git a/src/Init/Omega/Coeffs.lean b/src/Init/Omega/Coeffs.lean index b8f82bfc00..c7f511cb84 100644 --- a/src/Init/Omega/Coeffs.lean +++ b/src/Init/Omega/Coeffs.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Omega.IntList diff --git a/src/Init/Omega/Constraint.lean b/src/Init/Omega/Constraint.lean index d04dff9bf0..2d275ccb19 100644 --- a/src/Init/Omega/Constraint.lean +++ b/src/Init/Omega/Constraint.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Omega.LinearCombo import Init.Omega.Int diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean index e06da91f0f..97d5fd151b 100644 --- a/src/Init/Omega/Int.lean +++ b/src/Init/Omega/Int.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.Int.DivMod.Bootstrap import Init.Data.Int.Order diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean index 83f437623d..68ad776f29 100644 --- a/src/Init/Omega/IntList.lean +++ b/src/Init/Omega/IntList.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Data.List.Zip import Init.Data.Int.DivMod.Bootstrap diff --git a/src/Init/Omega/LinearCombo.lean b/src/Init/Omega/LinearCombo.lean index 0cf5fd20e3..e03d820efb 100644 --- a/src/Init/Omega/LinearCombo.lean +++ b/src/Init/Omega/LinearCombo.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.Omega.Coeffs import Init.Data.ToString.Macro diff --git a/src/Init/Omega/Logic.lean b/src/Init/Omega/Logic.lean index b5b8c0b16e..998e2b2517 100644 --- a/src/Init/Omega/Logic.lean +++ b/src/Init/Omega/Logic.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ +module + prelude import Init.PropLemmas /-! diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 6784e6d7df..0bb3f10af2 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude -- Don't import Init, because we're in Init itself set_option linter.missingDocs true -- keep it documented diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index 258730e5d9..0f925e5b08 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -6,6 +6,8 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Mario Carneiro This provides additional lemmas about propositional types beyond what is needed for Core and SimpLemmas. -/ +module + prelude import Init.Core import Init.NotationExtra diff --git a/src/Init/RCases.lean b/src/Init/RCases.lean index b4c7d33a14..2429e9c6ba 100644 --- a/src/Init/RCases.lean +++ b/src/Init/RCases.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Jacob von Raumer -/ +module + prelude import Init.Tactics import Init.Meta diff --git a/src/Init/ShareCommon.lean b/src/Init/ShareCommon.lean index e0addaf813..d25450ecac 100644 --- a/src/Init/ShareCommon.lean +++ b/src/Init/ShareCommon.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Util import Init.Data.UInt.Basic diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 5fd578af7b..4649138283 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -5,6 +5,8 @@ Authors: Leonardo de Moura notation, basic datatypes and type classes -/ +module + prelude import Init.Core set_option linter.missingDocs true -- keep it documented diff --git a/src/Init/Simproc.lean b/src/Init/Simproc.lean index a679681364..066492f1c7 100644 --- a/src/Init/Simproc.lean +++ b/src/Init/Simproc.lean @@ -3,6 +3,8 @@ Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.NotationExtra diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean index 8be04fd32b..2d116ba72f 100644 --- a/src/Init/SizeOf.lean +++ b/src/Init/SizeOf.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Tactics set_option linter.missingDocs true -- keep it documented diff --git a/src/Init/SizeOfLemmas.lean b/src/Init/SizeOfLemmas.lean index 516f1a1f56..9e67080a3e 100644 --- a/src/Init/SizeOfLemmas.lean +++ b/src/Init/SizeOfLemmas.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Meta import Init.SizeOf diff --git a/src/Init/Syntax.lean b/src/Init/Syntax.lean index 9006a16962..368a54c9c2 100644 --- a/src/Init/Syntax.lean +++ b/src/Init/Syntax.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Data.Array.Set diff --git a/src/Init/System.lean b/src/Init/System.lean index 8c0766bc23..097803f436 100644 --- a/src/Init/System.lean +++ b/src/Init/System.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.System.IO import Init.System.Platform diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean index 8c41290bc5..b8e1c2b5e4 100644 --- a/src/Init/System/FilePath.lean +++ b/src/Init/System/FilePath.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ +module + prelude import Init.System.Platform import Init.Data.ToString.Basic diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 5dbaad1fa6..a84bf44efd 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone -/ +module + prelude import Init.System.IOError import Init.System.FilePath diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean index 84e57c786b..6356f13ef8 100644 --- a/src/Init/System/IOError.lean +++ b/src/Init/System/IOError.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Simon Hudon -/ +module + prelude import Init.Data.ToString.Basic diff --git a/src/Init/System/Mutex.lean b/src/Init/System/Mutex.lean index c081be44a4..e383e48aac 100644 --- a/src/Init/System/Mutex.lean +++ b/src/Init/System/Mutex.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ +module + prelude import Init.System.IO import Init.Control.StateRef diff --git a/src/Init/System/Platform.lean b/src/Init/System/Platform.lean index 9ee351ac46..5681a27398 100644 --- a/src/Init/System/Platform.lean +++ b/src/Init/System/Platform.lean @@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.Nat.Basic import Init.Data.String.Basic diff --git a/src/Init/System/Promise.lean b/src/Init/System/Promise.lean index 5f5e451266..15d37e3445 100644 --- a/src/Init/System/Promise.lean +++ b/src/Init/System/Promise.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ +module + prelude import Init.System.IO diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean index a8aba27643..c8a317c3c0 100644 --- a/src/Init/System/ST.lean +++ b/src/Init/System/ST.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Classical import Init.Control.EState diff --git a/src/Init/System/Uri.lean b/src/Init/System/Uri.lean index 0361183909..8ea32db8b0 100644 --- a/src/Init/System/Uri.lean +++ b/src/Init/System/Uri.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Lovett -/ +module + prelude import Init.Data.String.Extra import Init.Data.Nat.Linear diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index d68bd3eaae..1d8eb3dbff 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Notation set_option linter.missingDocs true -- keep it documented diff --git a/src/Init/TacticsExtra.lean b/src/Init/TacticsExtra.lean index 425f9a619f..b4736179bf 100644 --- a/src/Init/TacticsExtra.lean +++ b/src/Init/TacticsExtra.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ +module + prelude import Init.Tactics import Init.NotationExtra diff --git a/src/Init/Task.lean b/src/Init/Task.lean index 47f5cc40e0..8f99e4bba5 100644 --- a/src/Init/Task.lean +++ b/src/Init/Task.lean @@ -5,6 +5,8 @@ Authors: Sebastian Ullrich Additional `Task` definitions. -/ +module + prelude import Init.Core import Init.Data.List.Basic diff --git a/src/Init/Try.lean b/src/Init/Try.lean index 612b3daaf8..9e23477a67 100644 --- a/src/Init/Try.lean +++ b/src/Init/Try.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Tactics diff --git a/src/Init/Util.lean b/src/Init/Util.lean index 40f37b01d9..69ba0eecfb 100644 --- a/src/Init/Util.lean +++ b/src/Init/Util.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Data.String.Basic import Init.Data.ToString.Basic diff --git a/src/Init/WF.lean b/src/Init/WF.lean index f2c71501eb..1ebd8b03ff 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.SizeOf import Init.BinderNameHint diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index cc49dcf42c..84a7c2ce1e 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ +module + prelude import Init.SizeOf import Init.MetaTypes diff --git a/src/Init/While.lean b/src/Init/While.lean index 1264cdad4c..726593d632 100644 --- a/src/Init/While.lean +++ b/src/Init/While.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +module + prelude import Init.Core diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp index 715c7e2493..786eca5d06 100644 --- a/src/runtime/compact.cpp +++ b/src/runtime/compact.cpp @@ -387,15 +387,10 @@ compacted_region::compacted_region(size_t sz, void * data, void * base_addr, boo m_end(static_cast(data)+sz) { } -compacted_region::compacted_region(object_compactor const & c): - m_begin(malloc(c.size())), - m_next(m_begin), - m_end(static_cast(m_begin) + c.size()) { - memcpy(m_begin, c.data(), c.size()); -} - compacted_region::~compacted_region() { - m_free_data(); + if (m_free_data) { + m_free_data(); + } } inline object * compacted_region::fix_object_ptr(object * o) { diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 45eeef1254..a157235ebf 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -36,6 +36,10 @@ find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 echo -n 'bytes .olean: ' find ${BUILD:-build/release}/stage2/lib/lean -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 + echo -n 'bytes .olean.server: ' + find ${BUILD:-build/release}/stage2/lib/lean -name '*.olean.server' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 + echo -n 'bytes .olean.private: ' + find ${BUILD:-build/release}/stage2/lib/lean -name '*.olean.private' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 echo -n 'lines C: ' find ${BUILD:-build/release}/stage2/lib/temp -name '*.c' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 echo -n 'lines C++: ' @@ -53,10 +57,10 @@ set -euxo pipefail echo -n 'bytes .olean: ' find ${BUILD:-build/release}/stage2/lib/lean/Init -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 - #echo -n 'bytes .olean.server: ' - #find ${BUILD:-build/release}/stage2/lib/lean/Init -name '*.olean.server' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 - #echo -n 'bytes .olean.private: ' - #find ${BUILD:-build/release}/stage2/lib/lean/Init -name '*.olean.private' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 + echo -n 'bytes .olean.server: ' + find ${BUILD:-build/release}/stage2/lib/lean/Init -name '*.olean.server' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 + echo -n 'bytes .olean.private: ' + find ${BUILD:-build/release}/stage2/lib/lean/Init -name '*.olean.private' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 max_runs: 1 runner: output - attributes: @@ -74,42 +78,42 @@ tags: [fast] run_config: <<: *time - cmd: lean ../../src/Init/Prelude.lean + cmd: lean -Dexperimental.module=true ../../src/Init/Prelude.lean - attributes: description: Init.Data.List.Sublist async tags: [fast] run_config: <<: *time - cmd: lean ../../src/Init/Data/List/Sublist.lean + cmd: lean -Dexperimental.module=true ../../src/Init/Data/List/Sublist.lean - attributes: description: Std.Data.Internal.List.Associative tags: [fast] run_config: <<: *time - cmd: lean ../../src/Std/Data/Internal/List/Associative.lean + cmd: lean -Dexperimental.module=true ../../src/Std/Data/Internal/List/Associative.lean - attributes: description: Std.Data.DHashMap.Internal.RawLemmas tags: [fast] run_config: <<: *time - cmd: lean ../../src/Std/Data/DHashMap/Internal/RawLemmas.lean + cmd: lean -Dexperimental.module=true ../../src/Std/Data/DHashMap/Internal/RawLemmas.lean - attributes: description: Init.Data.BitVec.Lemmas tags: [fast] run_config: <<: *time - cmd: lean ../../src/Init/Data/BitVec/Lemmas.lean + cmd: lean -Dexperimental.module=true ../../src/Init/Data/BitVec/Lemmas.lean - attributes: description: Init.Data.List.Sublist re-elab -j4 run_config: <<: *time - cmd: lean --run ../../script/benchReelabRss.lean lean ../../src/Init/Data/List/Sublist.lean 10 -j4 + cmd: lean --run ../../script/benchReelabRss.lean lean ../../src/Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true max_runs: 2 - attributes: description: Init.Data.BitVec.Lemmas re-elab run_config: <<: *time - cmd: lean --run ../../script/benchReelabRss.lean lean ../../src/Init/Data/BitVec/Lemmas.lean 2 -j4 + cmd: lean --run ../../script/benchReelabRss.lean lean ../../src/Init/Data/BitVec/Lemmas.lean 2 -j4 -Dexperimental.module=true max_runs: 2 - attributes: description: import Lean