digama0 · srghma · May 17, 2026
diff --git a/Lean4Lean.lean b/Lean4Lean.lean
@@ -1,3 +1,5 @@
+module
+prelude
 import Lean4Lean.Environment
 
 /-

diff --git a/Lean4Lean/Declaration.lean b/Lean4Lean/Declaration.lean
@@ -1,4 +1,8 @@
-import Lean.Declaration
+module
+
+public import Lean.Declaration
+
+@[expose] public section
 
 
 namespace Lean

diff --git a/Lean4Lean/Environment.lean b/Lean4Lean/Environment.lean
@@ -1,7 +1,11 @@
-import Lean4Lean.TypeChecker
-import Lean4Lean.Quot
-import Lean4Lean.Inductive.Add
-import Lean4Lean.Primitive
+module
+
+public import Lean4Lean.TypeChecker
+public import Lean4Lean.Quot
+public import Lean4Lean.Inductive.Add
+public import Lean4Lean.Primitive
+
+@[expose] public section
 
 namespace Lean4Lean
 open Lean hiding Environment Exception

diff --git a/Lean4Lean/Environment/Basic.lean b/Lean4Lean/Environment/Basic.lean
@@ -1,5 +1,9 @@
-import Lean.Environment
-import Batteries.Tactic.OpenPrivate
+module
+
+public import Lean.Environment
+public import Batteries.Tactic.OpenPrivate
+
+@[expose] public section
 
 namespace Lean.Kernel.Environment
 

diff --git a/Lean4Lean/EquivManager.lean b/Lean4Lean/EquivManager.lean
@@ -1,5 +1,9 @@
-import Batteries.Data.UnionFind.Basic
-import Lean4Lean.PtrEq
+module
+
+public import Batteries.Data.UnionFind.Basic
+public import Lean4Lean.PtrEq
+
+@[expose] public section
 
 namespace Lean4Lean
 open Lean

diff --git a/Lean4Lean/Experimental/CoinductiveLogRel.lean b/Lean4Lean/Experimental/CoinductiveLogRel.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Theory.Typing.HeadReduction
+module
+
+public import Lean4Lean.Theory.Typing.HeadReduction
+
+@[expose] public section
 
 namespace Lean4Lean
 namespace VEnv

diff --git a/Lean4Lean/Experimental/DomainTheory.lean b/Lean4Lean/Experimental/DomainTheory.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Experimental.SExpr
+module
+
+public import Lean4Lean.Experimental.SExpr
+
+@[expose] public section
 
 namespace Lean4Lean
 

diff --git a/Lean4Lean/Experimental/LogRel.lean b/Lean4Lean/Experimental/LogRel.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Experimental.SExpr
+module
+
+public import Lean4Lean.Experimental.SExpr
+
+@[expose] public section
 
 namespace Lean4Lean
 

diff --git a/Lean4Lean/Experimental/MoreStepIndexed.lean b/Lean4Lean/Experimental/MoreStepIndexed.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Experimental.SExpr
+module
+
+public import Lean4Lean.Experimental.SExpr
+
+@[expose] public section
 
 namespace Lean4Lean
 

diff --git a/Lean4Lean/Experimental/NormalEq.lean b/Lean4Lean/Experimental/NormalEq.lean
@@ -1,5 +1,9 @@
-import Lean4Lean.Theory.Typing.Lemmas
-import Lean4Lean.Theory.Typing.Pattern
+module
+
+public import Lean4Lean.Theory.Typing.Lemmas
+public import Lean4Lean.Theory.Typing.Pattern
+
+@[expose] public section
 
 -- TODO: remove, this is now part of ChurchRosser.lean
 

diff --git a/Lean4Lean/Experimental/ParallelReduction.lean b/Lean4Lean/Experimental/ParallelReduction.lean
@@ -1,5 +1,9 @@
-import Lean4Lean.Theory.Typing.Strong
-import Lean4Lean.Experimental.NormalEq
+module
+
+public import Lean4Lean.Theory.Typing.Strong
+public import Lean4Lean.Experimental.NormalEq
+
+@[expose] public section
 
 -- TODO: remove, this is now part of ChurchRosser.lean
 

diff --git a/Lean4Lean/Experimental/SExpr.lean b/Lean4Lean/Experimental/SExpr.lean
@@ -1,5 +1,9 @@
-import Lean4Lean.Theory.Typing.Lemmas
-import Lean4Lean.Theory.Typing.Pattern
+module
+
+public import Lean4Lean.Theory.Typing.Lemmas
+public import Lean4Lean.Theory.Typing.Pattern
+
+@[expose] public section
 
 namespace Lean4Lean
 

diff --git a/Lean4Lean/Experimental/ShapeLogRel.lean b/Lean4Lean/Experimental/ShapeLogRel.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Experimental.SExpr
+module
+
+public import Lean4Lean.Experimental.SExpr
+
+@[expose] public section
 
 namespace Lean4Lean
 

diff --git a/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean b/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Experimental.ShapeLogRel
+module
+
+public import Lean4Lean.Experimental.ShapeLogRel
+
+@[expose] public section
 
 namespace Lean4Lean
 

diff --git a/Lean4Lean/Experimental/StepIndexed.lean b/Lean4Lean/Experimental/StepIndexed.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Experimental.SExpr
+module
+
+public import Lean4Lean.Experimental.SExpr
+
+@[expose] public section
 
 namespace Lean4Lean
 

diff --git a/Lean4Lean/Experimental/Stratified.lean b/Lean4Lean/Experimental/Stratified.lean
@@ -1,5 +1,9 @@
-import Lean4Lean.Theory.Typing.Lemmas
-import Lean4Lean.Theory.Typing.Strong
+module
+
+public import Lean4Lean.Theory.Typing.Lemmas
+public import Lean4Lean.Theory.Typing.Strong
+
+@[expose] public section
 
 namespace Lean4Lean
 namespace VEnv

diff --git a/Lean4Lean/Experimental/StratifiedUntyped.lean b/Lean4Lean/Experimental/StratifiedUntyped.lean
@@ -1,5 +1,9 @@
-import Lean4Lean.Theory.Typing.Lemmas
-import Lean4Lean.Theory.Typing.Strong
+module
+
+public import Lean4Lean.Theory.Typing.Lemmas
+public import Lean4Lean.Theory.Typing.Strong
+
+@[expose] public section
 
 namespace Lean4Lean
 namespace VEnv

diff --git a/Lean4Lean/Experimental/Stronger.lean b/Lean4Lean/Experimental/Stronger.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Theory.Typing.Lemmas
+module
+
+public import Lean4Lean.Theory.Typing.Lemmas
+
+@[expose] public section
 
 namespace Lean4Lean
 

diff --git a/Lean4Lean/Experimental/Thierry.lean b/Lean4Lean/Experimental/Thierry.lean
@@ -1,3 +1,7 @@
+module
+
+@[expose] public section
+
 /-!
 # Partial formalization of Coquand & Huber, "An Adequacy Theorem for Dependent Type Theory"
 https://doi.org/10.1007/s00224-018-9879-9

diff --git a/Lean4Lean/Experimental/Thierry2.lean b/Lean4Lean/Experimental/Thierry2.lean
@@ -1,3 +1,5 @@
+module
+
 /-!
 # Partial formalization of Coquand & Huber, "An Adequacy Theorem for Dependent Type Theory"
 https://doi.org/10.1007/s00224-018-9879-9
@@ -829,3 +831,5 @@ theorem DefEqLamF.mono_r : DefEqF (n := n) B B .U a .U → DefEqPiF DefEqF B F F
 termination_by 2 * n + 1
 
 end
+
+@[expose] public section
diff --git a/Lean4Lean/Experimental/UniqueTyping.lean b/Lean4Lean/Experimental/UniqueTyping.lean
@@ -1,4 +1,8 @@
-import Lean4Lean.Experimental.ShapeLogRelAdequacy
+module
+
+public import Lean4Lean.Experimental.ShapeLogRelAdequacy
+
+@[expose] public section
 
 /-! # Unique typing over the SExpr weak defeq.
 

diff --git a/Lean4Lean/Expr.lean b/Lean4Lean/Expr.lean
@@ -1,4 +1,8 @@
-import Lean.Environment
+module
+
+public import Lean.Environment
+
+@[expose] public section
 
 namespace Lean
 namespace Expr

diff --git a/Lean4Lean/ForEachExprV.lean b/Lean4Lean/ForEachExprV.lean
@@ -1,5 +1,9 @@
-import Lean.Expr
-import Lean.Util.MonadCache
+module
+
+public import Lean.Expr
+public import Lean.Util.MonadCache
+
+@[expose] public section
 
 /-!
 This is the same as `Expr.forEach` but it uses `StateT` instead of `StateRefT` to avoid opaques.

diff --git a/Lean4Lean/Inductive/Add.lean b/Lean4Lean/Inductive/Add.lean
@@ -1,6 +1,10 @@
-import Batteries.Data.List.Basic
-import Lean4Lean.Environment.Basic
-import Lean4Lean.TypeChecker
+module
+
+public import Batteries.Data.List.Basic
+public import Lean4Lean.Environment.Basic
+public import Lean4Lean.TypeChecker
+
+@[expose] public section
 
 namespace Lean4Lean
 open Lean hiding Environment Exception

diff --git a/Lean4Lean/Inductive/Reduce.lean b/Lean4Lean/Inductive/Reduce.lean
@@ -1,6 +1,10 @@
-import Lean.Structure
-import Lean4Lean.Expr
-import Lean4Lean.Environment.Basic
+module
+
+public import Lean.Structure
+public import Lean4Lean.Expr
+public import Lean4Lean.Environment.Basic
+
+@[expose] public section
 
 namespace Lean4Lean
 open Lean hiding Environment

diff --git a/Lean4Lean/Instantiate.lean b/Lean4Lean/Instantiate.lean
@@ -1,6 +1,10 @@
-import Lean.Expr
-import Lean.LocalContext
-import Lean.Util.InstantiateLevelParams
+module
+
+public import Lean.Expr
+public import Lean.LocalContext
+public import Lean.Util.InstantiateLevelParams
+
+@[expose] public section
 
 namespace Lean
 namespace Expr

diff --git a/Lean4Lean/Level.lean b/Lean4Lean/Level.lean
@@ -1,5 +1,9 @@
-import Lean
-import Lean4Lean.List
+module
+
+public import Lean
+public import Lean4Lean.List
+
+@[expose] public section
 
 namespace Lean.Level
 

diff --git a/Lean4Lean/List.lean b/Lean4Lean/List.lean
@@ -1,3 +1,6 @@
+module
+
+@[expose] public section
 
 @[specialize] def List.all2 (R : α → α → Bool) : List α → List α → Bool
   | a1 :: as1, a2 :: as2 => R a1 a2 && all2 R as1 as2

diff --git a/Lean4Lean/LocalContext.lean b/Lean4Lean/LocalContext.lean
@@ -1,4 +1,8 @@
-import Lean.LocalContext
+module
+
+public import Lean.LocalContext
+
+@[expose] public section
 
 namespace Lean4Lean
 open Lean

diff --git a/Lean4Lean/Primitive.lean b/Lean4Lean/Primitive.lean
@@ -1,5 +1,9 @@
-import Lean4Lean.TypeChecker
-import Lean4Lean.Environment.Basic
+module
+
+public import Lean4Lean.TypeChecker
+public import Lean4Lean.Environment.Basic
+
+@[expose] public section
 
 namespace Lean4Lean
 namespace Environment

diff --git a/Lean4Lean/PtrEq.lean b/Lean4Lean/PtrEq.lean
@@ -1,4 +1,8 @@
-import Lean.Declaration
+module
+
+public import Lean.Declaration
+
+@[expose] public section
 
 namespace Lean4Lean
 open Lean

diff --git a/Lean4Lean/Quot.lean b/Lean4Lean/Quot.lean
@@ -1,8 +1,12 @@
-import Batteries.Tactic.OpenPrivate
-import Lean4Lean.Environment.Basic
-import Lean4Lean.Expr
-import Lean4Lean.Instantiate
-import Lean4Lean.LocalContext
+module
+
+public import Batteries.Tactic.OpenPrivate
+public import Lean4Lean.Environment.Basic
+public import Lean4Lean.Expr
+public import Lean4Lean.Instantiate
+public import Lean4Lean.LocalContext
+
+@[expose] public section
 
 namespace Lean4Lean
 open Lean hiding Environment Exception

diff --git a/Lean4Lean/Std/Basic.lean b/Lean4Lean/Std/Basic.lean
@@ -1,8 +1,12 @@
-import Batteries.CodeAction
-import Batteries.Data.Array.Lemmas
-import Batteries.Data.HashMap.Basic
-import Batteries.Data.UnionFind.Basic
-import Batteries.Tactic.SeqFocus
+module
+
+public import Batteries.CodeAction
+public import Batteries.Data.Array.Lemmas
+public import Batteries.Data.HashMap.Basic
+public import Batteries.Data.UnionFind.Basic
+public import Batteries.Tactic.SeqFocus
+
+@[expose] public section
 
 open Std
 

diff --git a/Lean4Lean/Std/Control.lean b/Lean4Lean/Std/Control.lean
@@ -1,2 +1,6 @@
+module
+
 
 instance [Alternative m] : MonadLift Option m := ⟨fun | none => failure | some a => pure a⟩
+
+@[expose] public section
diff --git a/Lean4Lean/Std/HashMap.lean b/Lean4Lean/Std/HashMap.lean
@@ -1,5 +1,9 @@
-import Std.Data.HashMap.Lemmas
-import Lean
+module
+
+public import Std.Data.HashMap.Lemmas
+public import Lean
+
+@[expose] public section
 
 namespace Std.Internal.List
-Original file line number
+Diff line change
@@ -1,3 +1,5 @@
+    module
+    prelude
     import Lean4Lean.Environment
     /-
@@ Expand Down @@