perf: add prelude to all Lean modules

2026-04-12 15:14:07 +00:00 · 2024-02-18 14:46:39 -08:00
543 changed files with 622 additions and 25 deletions
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.CoreM
 import Lean.MonadEnv

--- a/src/Lean/AuxRecursor.lean
+++ b/src/Lean/AuxRecursor.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment

 namespace Lean
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Attributes

 namespace Lean
--- a/src/Lean/Compiler.lean
+++ b/src/Lean/Compiler.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.InlineAttrs
 import Lean.Compiler.Specialize
 import Lean.Compiler.ConstFolding
--- a/src/Lean/Compiler/AtMostOnce.lean
+++ b/src/Lean/Compiler/AtMostOnce.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment

 namespace Lean.Compiler
--- a/src/Lean/Compiler/BorrowedAnnotation.lean
+++ b/src/Lean/Compiler/BorrowedAnnotation.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Expr
 namespace Lean

--- a/src/Lean/Compiler/CSimpAttr.lean
+++ b/src/Lean/Compiler/CSimpAttr.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.ScopedEnvExtension
 import Lean.Util.Recognizers
 import Lean.Util.ReplaceExpr
--- a/src/Lean/Compiler/ClosedTermCache.lean
+++ b/src/Lean/Compiler/ClosedTermCache.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment

 namespace Lean
--- a/src/Lean/Compiler/ConstFolding.lean
+++ b/src/Lean/Compiler/ConstFolding.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Expr

 /-! Constant folding for primitives that have special runtime support. -/
--- a/src/Lean/Compiler/ExportAttr.lean
+++ b/src/Lean/Compiler/ExportAttr.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Attributes

 namespace Lean
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.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
 -/
+prelude
+import Init.Data.List.BasicAux
 import Lean.Expr
 import Lean.Environment
 import Lean.Attributes
--- a/src/Lean/Compiler/FFI.lean
+++ b/src/Lean/Compiler/FFI.lean
@@ -3,6 +3,9 @@ Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+prelude
+import Init.Data.Array.Basic
+import Init.System.FilePath

 open System

--- a/src/Lean/Compiler/IR.lean
+++ b/src/Lean/Compiler/IR.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.Format
 import Lean.Compiler.IR.CompilerM
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Data.KVMap
 import Lean.Data.Name
 import Lean.Data.Format
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.ExportAttr
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.NormIds
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Runtime
 import Lean.Compiler.ClosedTermCache
 import Lean.Compiler.ExternAttr
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.Format

--- a/src/Lean/Compiler/IR/CompilerM.lean
+++ b/src/Lean/Compiler/IR/CompilerM.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.Format
--- a/src/Lean/Compiler/IR/CtorLayout.lean
+++ b/src/Lean/Compiler/IR/CtorLayout.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment
 import Lean.Compiler.IR.Format

--- a/src/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Format
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.CompilerM
--- a/src/Lean/Compiler/IR/ElimDeadVars.lean
+++ b/src/Lean/Compiler/IR/ElimDeadVars.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.FreeVars

--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Runtime
 import Lean.Compiler.NameMangling
 import Lean.Compiler.ExportAttr
--- a/src/Lean/Compiler/IR/EmitLLVM.lean
+++ b/src/Lean/Compiler/IR/EmitLLVM.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
-
+prelude
 import Lean.Data.HashMap
 import Lean.Runtime
 import Lean.Compiler.NameMangling
--- a/src/Lean/Compiler/IR/EmitUtil.lean
+++ b/src/Lean/Compiler/IR/EmitUtil.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.InitAttr
 import Lean.Compiler.IR.CompilerM

--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.NormIds
 import Lean.Compiler.IR.FreeVars
--- a/src/Lean/Compiler/IR/Format.lean
+++ b/src/Lean/Compiler/IR/Format.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic

 namespace Lean
--- a/src/Lean/Compiler/IR/FreeVars.lean
+++ b/src/Lean/Compiler/IR/FreeVars.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic

 namespace Lean.IR
--- a/src/Lean/Compiler/IR/LLVMBindings.lean
+++ b/src/Lean/Compiler/IR/LLVMBindings.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: Siddharth Bhat
 -/
+prelude
+import Init.System.IO

 namespace LLVM
 /-!
--- a/src/Lean/Compiler/IR/LiveVars.lean
+++ b/src/Lean/Compiler/IR/LiveVars.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.FreeVars

--- a/src/Lean/Compiler/IR/NormIds.lean
+++ b/src/Lean/Compiler/IR/NormIds.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic

 namespace Lean.IR.UniqueIds
--- a/src/Lean/Compiler/IR/PushProj.lean
+++ b/src/Lean/Compiler/IR/PushProj.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.FreeVars
 import Lean.Compiler.IR.NormIds
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Runtime
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.LiveVars
--- a/src/Lean/Compiler/IR/ResetReuse.lean
+++ b/src/Lean/Compiler/IR/ResetReuse.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.LiveVars
 import Lean.Compiler.IR.Format
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.Format

--- a/src/Lean/Compiler/IR/Sorry.lean
+++ b/src/Lean/Compiler/IR/Sorry.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.CompilerM

 namespace Lean.IR
--- a/src/Lean/Compiler/IR/UnboxResult.lean
+++ b/src/Lean/Compiler/IR/UnboxResult.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Data.Format
 import Lean.Compiler.IR.Basic

--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/src/Lean/Compiler/ImplementedByAttr.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Attributes
 import Lean.Declaration
 import Lean.MonadEnv
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Elab.InfoTree.Main

 namespace Lean
--- a/src/Lean/Compiler/InlineAttrs.lean
+++ b/src/Lean/Compiler/InlineAttrs.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Attributes


--- a/src/Lean/Compiler/LCNF.lean
+++ b/src/Lean/Compiler/LCNF.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.AlphaEqv
 import Lean.Compiler.LCNF.Basic
 import Lean.Compiler.LCNF.Bind
--- a/src/Lean/Compiler/LCNF/AlphaEqv.lean
+++ b/src/Lean/Compiler/LCNF/AlphaEqv.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/AuxDeclCache.lean
+++ b/src/Lean/Compiler/LCNF/AuxDeclCache.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.DeclHash
 import Lean.Compiler.LCNF.Internalize
--- a/src/Lean/Compiler/LCNF/BaseTypes.lean
+++ b/src/Lean/Compiler/LCNF/BaseTypes.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.Types

--- a/src/Lean/Compiler/LCNF/Basic.lean
+++ b/src/Lean/Compiler/LCNF/Basic.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
 -/
+prelude
+import Init.Data.List.BasicAux
 import Lean.Expr
 import Lean.Meta.Instances
 import Lean.Compiler.InlineAttrs
--- a/src/Lean/Compiler/LCNF/Bind.lean
+++ b/src/Lean/Compiler/LCNF/Bind.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.InferType

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/CSE.lean
+++ b/src/Lean/Compiler/LCNF/CSE.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.ToExpr
 import Lean.Compiler.LCNF.PassManager
--- a/src/Lean/Compiler/LCNF/Check.lean
+++ b/src/Lean/Compiler/LCNF/Check.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.InferType
 import Lean.Compiler.LCNF.PrettyPrinter
 import Lean.Compiler.LCNF.CompatibleTypes
--- a/src/Lean/Compiler/LCNF/Closure.lean
+++ b/src/Lean/Compiler/LCNF/Closure.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Util.ForEachExprWhere
 import Lean.Compiler.LCNF.CompilerM

--- a/src/Lean/Compiler/LCNF/CompatibleTypes.lean
+++ b/src/Lean/Compiler/LCNF/CompatibleTypes.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.InferType

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/CompilerM.lean
+++ b/src/Lean/Compiler/LCNF/CompilerM.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.CoreM
 import Lean.Compiler.LCNF.Basic
 import Lean.Compiler.LCNF.LCtx
--- a/src/Lean/Compiler/LCNF/ConfigOptions.lean
+++ b/src/Lean/Compiler/LCNF/ConfigOptions.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Data.Options

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/DeclHash.lean
+++ b/src/Lean/Compiler/LCNF/DeclHash.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/DependsOn.lean
+++ b/src/Lean/Compiler/LCNF/DependsOn.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/ElimDead.lean
+++ b/src/Lean/Compiler/LCNF/ElimDead.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.PhaseExt
--- a/src/Lean/Compiler/LCNF/FVarUtil.lean
+++ b/src/Lean/Compiler/LCNF/FVarUtil.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Expr
 import Lean.Compiler.LCNF.Basic
 import Lean.Compiler.LCNF.CompilerM
--- a/src/Lean/Compiler/LCNF/FixedParams.lean
+++ b/src/Lean/Compiler/LCNF/FixedParams.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic
 import Lean.Compiler.LCNF.Types

--- a/src/Lean/Compiler/LCNF/FloatLetIn.lean
+++ b/src/Lean/Compiler/LCNF/FloatLetIn.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.FVarUtil
 import Lean.Compiler.LCNF.PassManager
--- a/src/Lean/Compiler/LCNF/ForEachExpr.lean
+++ b/src/Lean/Compiler/LCNF/ForEachExpr.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Util.ForEachExpr
 import Lean.Compiler.LCNF.Basic

--- a/src/Lean/Compiler/LCNF/InferType.lean
+++ b/src/Lean/Compiler/LCNF/InferType.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.PhaseExt
--- a/src/Lean/Compiler/LCNF/Internalize.lean
+++ b/src/Lean/Compiler/LCNF/Internalize.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Bind
 import Lean.Compiler.LCNF.CompilerM
--- a/src/Lean/Compiler/LCNF/JoinPoints.lean
+++ b/src/Lean/Compiler/LCNF/JoinPoints.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.PullFunDecls
--- a/src/Lean/Compiler/LCNF/LCtx.lean
+++ b/src/Lean/Compiler/LCNF/LCtx.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.LocalContext
 import Lean.Compiler.LCNF.Basic

--- a/src/Lean/Compiler/LCNF/LambdaLifting.lean
+++ b/src/Lean/Compiler/LCNF/LambdaLifting.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Meta.Instances
 import Lean.Compiler.InlineAttrs
 import Lean.Compiler.LCNF.Closure
--- a/src/Lean/Compiler/LCNF/Level.lean
+++ b/src/Lean/Compiler/LCNF/Level.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Util.CollectLevelParams
 import Lean.Compiler.LCNF.Basic

--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.Options
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.Passes
--- a/src/Lean/Compiler/LCNF/MonadScope.lean
+++ b/src/Lean/Compiler/LCNF/MonadScope.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/MonoTypes.lean
+++ b/src/Lean/Compiler/LCNF/MonoTypes.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Meta.InferType
 import Lean.Compiler.LCNF.Util
 import Lean.Compiler.LCNF.BaseTypes
--- a/src/Lean/Compiler/LCNF/OtherDecl.lean
+++ b/src/Lean/Compiler/LCNF/OtherDecl.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.BaseTypes
 import Lean.Compiler.LCNF.MonoTypes

--- a/src/Lean/Compiler/LCNF/PassManager.lean
+++ b/src/Lean/Compiler/LCNF/PassManager.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Attributes
 import Lean.Environment
 import Lean.Meta.Basic
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/src/Lean/Compiler/LCNF/Passes.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.PullLetDecls
 import Lean.Compiler.LCNF.CSE
--- a/src/Lean/Compiler/LCNF/PhaseExt.lean
+++ b/src/Lean/Compiler/LCNF/PhaseExt.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.PassManager

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/PrettyPrinter.lean
+++ b/src/Lean/Compiler/LCNF/PrettyPrinter.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.PrettyPrinter
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.Internalize
--- a/src/Lean/Compiler/LCNF/Probing.lean
+++ b/src/Lean/Compiler/LCNF/Probing.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.PhaseExt
--- a/src/Lean/Compiler/LCNF/PullFunDecls.lean
+++ b/src/Lean/Compiler/LCNF/PullFunDecls.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.DependsOn
 import Lean.Compiler.LCNF.PassManager
--- a/src/Lean/Compiler/LCNF/PullLetDecls.lean
+++ b/src/Lean/Compiler/LCNF/PullLetDecls.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.DependsOn
 import Lean.Compiler.LCNF.Types
--- a/src/Lean/Compiler/LCNF/ReduceArity.lean
+++ b/src/Lean/Compiler/LCNF/ReduceArity.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.PhaseExt
 import Lean.Compiler.LCNF.InferType
--- a/src/Lean/Compiler/LCNF/ReduceJpArity.lean
+++ b/src/Lean/Compiler/LCNF/ReduceJpArity.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.InferType
 import Lean.Compiler.LCNF.PassManager
--- a/src/Lean/Compiler/LCNF/Renaming.lean
+++ b/src/Lean/Compiler/LCNF/Renaming.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/ScopeM.lean
+++ b/src/Lean/Compiler/LCNF/ScopeM.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/Simp.lean
+++ b/src/Lean/Compiler/LCNF/Simp.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.ReduceJpArity
 import Lean.Compiler.LCNF.Renaming
 import Lean.Compiler.LCNF.Simp.Basic
--- a/src/Lean/Compiler/LCNF/Simp/Basic.lean
+++ b/src/Lean/Compiler/LCNF/Simp/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Meta.Instances
 import Lean.Compiler.InlineAttrs
 import Lean.Compiler.Specialize
--- a/src/Lean/Compiler/LCNF/Simp/Config.lean
+++ b/src/Lean/Compiler/LCNF/Simp/Config.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
 -/
+prelude
+import Init.Core
 namespace Lean.Compiler.LCNF
 namespace Simp

--- a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean
+++ b/src/Lean/Compiler/LCNF/Simp/ConstantFold.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
 -/
+prelude
+import Init.Data.UInt.Log2
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.InferType
 import Lean.Compiler.LCNF.PassManager
--- a/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean
+++ b/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Simp.SimpM

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean
+++ b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.InferType
--- a/src/Lean/Compiler/LCNF/Simp/FunDeclInfo.lean
+++ b/src/Lean/Compiler/LCNF/Simp/FunDeclInfo.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Simp.Basic

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean
+++ b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Simp.SimpM

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/Simp/InlineProj.lean
+++ b/src/Lean/Compiler/LCNF/Simp/InlineProj.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Simp.SimpM

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/Simp/JpCases.lean
+++ b/src/Lean/Compiler/LCNF/Simp/JpCases.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.DependsOn
 import Lean.Compiler.LCNF.InferType
 import Lean.Compiler.LCNF.Internalize
--- a/src/Lean/Compiler/LCNF/Simp/Main.lean
+++ b/src/Lean/Compiler/LCNF/Simp/Main.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.ImplementedByAttr
 import Lean.Compiler.LCNF.ElimDead
 import Lean.Compiler.LCNF.AlphaEqv
--- a/src/Lean/Compiler/LCNF/Simp/SimpM.lean
+++ b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.ImplementedByAttr
 import Lean.Compiler.LCNF.Renaming
 import Lean.Compiler.LCNF.ElimDead
--- a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
+++ b/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Simp.SimpM

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/Simp/Used.lean
+++ b/src/Lean/Compiler/LCNF/Simp/Used.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Simp.SimpM

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/SpecInfo.lean
+++ b/src/Lean/Compiler/LCNF/SpecInfo.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.Specialize
 import Lean.Compiler.LCNF.FixedParams
 import Lean.Compiler.LCNF.InferType
--- a/src/Lean/Compiler/LCNF/Specialize.lean
+++ b/src/Lean/Compiler/LCNF/Specialize.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.Specialize
 import Lean.Compiler.LCNF.Simp
 import Lean.Compiler.LCNF.SpecInfo
--- a/src/Lean/Compiler/LCNF/Testing.lean
+++ b/src/Lean/Compiler/LCNF/Testing.lean
@@ -3,6 +3,7 @@ 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
 -/
+prelude
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.PrettyPrinter

--- a/src/Lean/Compiler/LCNF/ToDecl.lean
+++ b/src/Lean/Compiler/LCNF/ToDecl.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Meta.Transform
 import Lean.Meta.Match.MatcherInfo
 import Lean.Compiler.ImplementedByAttr
--- a/src/Lean/Compiler/LCNF/ToExpr.lean
+++ b/src/Lean/Compiler/LCNF/ToExpr.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic

 namespace Lean.Compiler.LCNF
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.ProjFns
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Compiler.LCNF.Types
--- a/Show More
+++ b/Show More