Adopt the module system

Auto.lean

@@ -1,4 +1,6 @@
-import Auto.Tactic
-import Auto.EvaluateAuto.TestAuto
-import Auto.EvaluateAuto.TestTactics
-import Auto.EvaluateAuto.TestTranslation
+module
+
+public import Auto.Tactic
+public import Auto.EvaluateAuto.TestAuto
+public import Auto.EvaluateAuto.TestTactics
+public import Auto.EvaluateAuto.TestTranslation

Auto/Debugger/Interactive.lean

@@ -1,4 +1,9 @@
-import Lean
+module
+
+public import Lean
+
+public section
+
 open Lean
 
 namespace Auto.Debugger

Auto/Debugger/RTrace.lean

@@ -1,4 +1,10 @@
-import Lean
+module
+
+public import Lean
+public meta import Lean
+
+public meta section
+
 open Lean
 
 namespace Auto.Debugger

Auto/Embedding/CoCBase.lean

@@ -1,5 +1,9 @@
-import Lean
-import Auto.Lib.TreeList
+module
+
+public import Lean
+public import Auto.Lib.TreeList
+
+@[expose] public section
 
 namespace Auto.Embedding.CoC
 

Auto/Embedding/LCtx.lean

@@ -1,9 +1,13 @@
-import Auto.Lib.BoolExtra
-import Auto.Lib.HEqExtra
-import Auto.Lib.NatExtra
-import Auto.Lib.ListExtra
-import Auto.Lib.HList
-import Auto.Lib.BinTree
+module
+
+public import Auto.Lib.BoolExtra
+public import Auto.Lib.HEqExtra
+public import Auto.Lib.NatExtra
+public import Auto.Lib.ListExtra
+public import Auto.Lib.HList
+public import Auto.Lib.BinTree
+
+@[expose] public section
 
 namespace Auto.Embedding
 

Auto/Embedding/LamBVarOp.lean

@@ -1,4 +1,8 @@
-import Auto.Embedding.LamBase
+module
+
+public import Auto.Embedding.LamBase
+
+@[expose] public section
 
 namespace Auto.Embedding.Lam
 
@@ -466,7 +470,7 @@ theorem LamTerm.maxEVarSucc_bvarLower?
   (heq : LamTerm.bvarLower? t = .some t') : t'.maxEVarSucc = t.maxEVarSucc :=
   LamTerm.maxEVarSucc_bvarLowersIdx? heq
 
-private def getILSortString : LamBaseTerm → String
+def getILSortString : LamBaseTerm → String
 | .eq s      => s!"{s}"
 | .forallE s => s!"{s}"
 | .existE s  => s!"{s}"

Auto/Embedding/LamBase.lean

@@ -1,14 +1,18 @@
-import Lean
-import Auto.Embedding.Lift
-import Auto.Embedding.LCtx
-import Auto.Embedding.LamConstMacro
-import Auto.Lib.ExprExtra
-import Auto.Lib.NatExtra
-import Auto.Lib.IntExtra
-import Auto.Lib.HEqExtra
-import Auto.Lib.ListExtra
+module
+
+public import Lean
+public import Auto.Embedding.Lift
+public import Auto.Embedding.LCtx
+public import Auto.Embedding.LamConstMacro
+public import Auto.Lib.ExprExtra
+public import Auto.Lib.NatExtra
+public import Auto.Lib.IntExtra
+public import Auto.Lib.HEqExtra
+public import Auto.Lib.ListExtra
 -- import Mathlib.Data.Real.Basic
-import Auto.MathlibEmulator
+public import Auto.MathlibEmulator
+
+@[expose] public section
 
 -- Embedding Simply Typed Lambda Calculus into Dependent Type Theory
 -- Simply Typed Lambda Calculus = HOL (without polymorphism)
@@ -2899,7 +2903,7 @@ def LamWF.bvarApps
       conv => enter [2, 3]; rw [tyeq]
       exact .ofBVar _)
 
-private def LamWF.bvarAppsRev_Aux :
+def LamWF.bvarAppsRev_Aux :
   LamWF ltv ⟨pushLCtxs (List.reverse lctx) (pushLCtx ty lctx'), LamTerm.bvar (List.length lctx), ty⟩ := by
   have tyeq : ty = pushLCtxs lctx.reverse (pushLCtx ty lctx') lctx.length := by
     rw [pushLCtxs_ge] <;> rw [List.length_reverse]

Auto/Embedding/LamBitVec.lean

@@ -1,5 +1,9 @@
-import Auto.Embedding.LamConv
-import Auto.Lib.NatExtra
+module
+
+public import Auto.Embedding.LamConv
+public import Auto.Lib.NatExtra
+
+@[expose] public section
 
 namespace Auto.Embedding.Lam
 

Auto/Embedding/LamChecker.lean

@@ -1,11 +1,16 @@
-import Auto.Embedding.LamTermInterp
-import Auto.Embedding.LamConv
-import Auto.Embedding.LamInference
-import Auto.Embedding.LamLCtx
-import Auto.Embedding.LamPrep
-import Auto.Embedding.LamBitVec
-import Auto.Embedding.LamInductive
-import Auto.Lib.BinTree
+module
+
+public import Auto.Embedding.LamTermInterp
+public import Auto.Embedding.LamConv
+public import Auto.Embedding.LamInference
+public import Auto.Embedding.LamLCtx
+public import Auto.Embedding.LamPrep
+public import Auto.Embedding.LamBitVec
+public import Auto.Embedding.LamInductive
+public import Auto.Lib.BinTree
+
+@[expose] public section
+
 open Lean
 
 namespace Auto.Embedding.Lam

Auto/Embedding/LamConstMacro.lean

@@ -1,4 +1,9 @@
-import Lean
+module
+
+public import Lean
+public meta import Lean
+
+public meta section
 
 /-!
 # `mkConstFamily` — macro for the constant-family scaffolding in `LamBase.lean`.

Auto/Embedding/LamConv.lean

@@ -1,4 +1,8 @@
-import Auto.Embedding.LamSystem
+module
+
+public import Auto.Embedding.LamSystem
+
+@[expose] public section
 
 namespace Auto.Embedding.Lam
 
@@ -856,7 +860,7 @@ def LamWF.instantiateAt
   | false => exact .ofBVar n
 | lctx, wfArg, .ofLam (argTy:=argTy') bodyTy' (body:=body') H =>
   let wfArg' := LamWF.bvarLiftIdx (s:=argTy') (lctx:=lctx) 0 _ wfArg
-  let IHArg := LamWF.instantiateAt ltv (Nat.succ idx) _
+  let IHArg := LamWF.instantiateAt (arg:=arg) (argTy:=argTy) ltv (Nat.succ idx) _
     (by
       dsimp [LamTerm.bvarLifts] at wfArg'
       rw [pushLCtxAt_zero, ← LamTerm.bvarLiftsIdx_succ_r] at wfArg'

Auto/Embedding/LamInductive.lean

@@ -1,4 +1,8 @@
-import Auto.Embedding.LamConv
+module
+
+public import Auto.Embedding.LamConv
+
+@[expose] public section
 
 namespace Auto.Embedding.Lam
 

Auto/Embedding/LamInference.lean

@@ -1,4 +1,8 @@
-import Auto.Embedding.LamConv
+module
+
+public import Auto.Embedding.LamConv
+
+@[expose] public section
 
 namespace Auto.Embedding.Lam
 

Auto/Embedding/LamInhReasoning.lean

@@ -1,4 +1,9 @@
-import Auto.Embedding.LamBase
+module
+
+public import Auto.Embedding.LamBase
+
+@[expose] public section
+
 open Lean
 
 namespace Auto.Embedding.Lam

Auto/Embedding/LamLCtx.lean

@@ -1,4 +1,8 @@
-import Auto.Embedding.LamSystem
+module
+
+public import Auto.Embedding.LamSystem
+
+@[expose] public section
 
 namespace Auto.Embedding.Lam
 

Auto/Embedding/LamPrep.lean

@@ -1,4 +1,8 @@
-import Auto.Embedding.LamConv
+module
+
+public import Auto.Embedding.LamConv
+
+@[expose] public section
 
 namespace Auto.Embedding.Lam
 

Auto/Embedding/LamSystem.lean

@@ -1,4 +1,8 @@
-import Auto.Embedding.LamBVarOp
+module
+
+public import Auto.Embedding.LamBVarOp
+
+@[expose] public section
 
 namespace Auto.Embedding.Lam
 

Auto/Embedding/LamTermInterp.lean

@@ -1,6 +1,11 @@
-import Auto.Embedding.LamSystem
-import Auto.Lib.MonadUtils
-import Auto.Lib.MetaState
+module
+
+public import Auto.Embedding.LamSystem
+public import Auto.Lib.MonadUtils
+public import Auto.Lib.MetaState
+
+@[expose] public section
+
 open Lean
 
 namespace Auto.Embedding.Lam

Auto/Embedding/Lift.lean

@@ -1,6 +1,10 @@
-import Auto.Lib.IsomType
-import Auto.Lib.StringExtra
-import Auto.Lib.BoolExtra
+module
+
+public import Auto.Lib.IsomType
+public import Auto.Lib.StringExtra
+public import Auto.Lib.BoolExtra
+
+@[expose] public section
 
 namespace Auto.Embedding
 

Auto/EvaluateAuto/AutoConfig.lean

@@ -1,5 +1,9 @@
-import Lean
-import Auto.Tactic
+module
+
+public import Lean
+public import Auto.Tactic
+
+public section
 
 open Lean Auto
 

Auto/EvaluateAuto/CommandAnalysis.lean

@@ -1,7 +1,12 @@
-import Lean
-import Auto.EvaluateAuto.EnvAnalysis
-import Auto.EvaluateAuto.ConstAnalysis
-import Auto.EvaluateAuto.Result
+module
+
+public import Lean
+public import Auto.EvaluateAuto.EnvAnalysis
+public import Auto.EvaluateAuto.ConstAnalysis
+public import Auto.EvaluateAuto.Result
+
+public section
+
 open Lean
 
 register_option auto.testTactics.ensureAesop : Bool := {

Auto/EvaluateAuto/ConstAnalysis.lean

@@ -1,4 +1,8 @@
-import Lean
+module
+
+public import Lean
+
+public section
 
 open Lean
 

Auto/EvaluateAuto/EnvAnalysis.lean

@@ -1,5 +1,9 @@
-import Lean
-import Auto.EvaluateAuto.NameArr
+module
+
+public import Lean
+public import Auto.EvaluateAuto.NameArr
+
+public section
 
 open Lean
 

Auto/EvaluateAuto/NameArr.lean

@@ -1,4 +1,9 @@
-import Lean
+module
+
+public import Lean
+
+public section
+
 open Lean
 
 namespace EvalAuto

Auto/EvaluateAuto/OS.lean

@@ -1,4 +1,8 @@
-import Lean
+module
+
+public import Lean
+
+public section
 
 open Lean
 

Auto/EvaluateAuto/Result.lean

@@ -1,4 +1,9 @@
-import Lean
+module
+
+public import Lean
+
+public section
+
 open Lean
 
 initialize

Auto/EvaluateAuto/TestAuto.lean

@@ -1,12 +1,25 @@
-import Lean
-import Std
-import Auto.EvaluateAuto.OS
-import Auto.EvaluateAuto.Result
-import Auto.EvaluateAuto.ConstAnalysis
-import Auto.EvaluateAuto.EnvAnalysis
-import Auto.EvaluateAuto.NameArr
-import Auto.EvaluateAuto.AutoConfig
-import Auto.Tactic
+module
+
+public import Lean
+public meta import Lean
+public import Std
+public meta import Std
+public import Auto.EvaluateAuto.OS
+public meta import Auto.EvaluateAuto.OS
+public import Auto.EvaluateAuto.Result
+public meta import Auto.EvaluateAuto.Result
+public import Auto.EvaluateAuto.ConstAnalysis
+public meta import Auto.EvaluateAuto.ConstAnalysis
+public import Auto.EvaluateAuto.EnvAnalysis
+public meta import Auto.EvaluateAuto.EnvAnalysis
+public import Auto.EvaluateAuto.NameArr
+public meta import Auto.EvaluateAuto.NameArr
+public import Auto.EvaluateAuto.AutoConfig
+public meta import Auto.EvaluateAuto.AutoConfig
+public import Auto.Tactic
+public meta import Auto.Tactic
+
+public meta section
 
 open Lean Auto