leanprover-community · sgraf812 · Feb 16, 2026 · Feb 17, 2026 · Feb 24, 2026 · Mar 1, 2026
diff --git a/Aesop/Builder/Apply.lean b/Aesop/Builder/Apply.lean
@@ -6,6 +6,7 @@ Authors: Jannis Limperg
 module
 
 public import Aesop.Builder.Basic
+import Batteries.Lean.Expr
 
 public section
 

diff --git a/Aesop/Builder/Cases.lean b/Aesop/Builder/Cases.lean
@@ -7,6 +7,7 @@ module
 
 public import Aesop.Builder.Basic
 public import Aesop.RuleTac.Cases
+import Batteries.Lean.Expr
 
 public section
 

diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean
@@ -28,7 +28,7 @@ namespace RuleBuilder
 
 def getForwardIndexingMode (type : Expr)
     (immediate : UnorderedArraySet PremiseIndex) : MetaM IndexingMode := do
-  let immediate := immediate.toArray.map (·.toNat)
+  let immediate := immediate.toArray.map PremiseIndex.toNat
   match immediate.max? with
   | some i =>
     withoutModifyingState do

diff --git a/Aesop/BuiltinRules/DestructProducts.lean b/Aesop/BuiltinRules/DestructProducts.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 module
 
+public meta import Lean.Meta.Tactic.Apply
 public import Aesop.Frontend.Attribute
 public import Aesop.Frontend.Extension
 public import Aesop.Frontend.RuleExpr

diff --git a/Aesop/ElabM.lean b/Aesop/ElabM.lean
@@ -5,7 +5,10 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Lean
+import Lean
+public import Lean.Expr
+public import Lean.Meta.Basic
+public import Lean.Elab.Term.TermElabM
 
 public section
 

diff --git a/Aesop/Exception.lean b/Aesop/Exception.lean
@@ -5,7 +5,7 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Lean
+import Lean.Exception
 
 public section
 

diff --git a/Aesop/Forward/Match.lean b/Aesop/Forward/Match.lean
@@ -5,6 +5,7 @@ Authors: Xavier Généreux, Jannis Limperg
 -/
 module
 
+import Lean.Meta.Tactic.Apply
 public import Aesop.Forward.Match.Types
 public import Aesop.Forward.PremiseIndex
 public import Aesop.Forward.SlotIndex
@@ -14,9 +15,8 @@ public import Aesop.RuleTac.Descr
 public import Aesop.RuleTac.ElabRuleTerm
 public import Aesop.RuleTac.Forward.Basic
 public import Aesop.Script.SpecificTactics
-public import Batteries.Lean.Meta.UnusedNames
+import Batteries.Lean.Meta.UnusedNames
 public import Aesop.Util.Basic
-public import Lean
 
 public section
 

diff --git a/Aesop/Forward/RuleInfo.lean b/Aesop/Forward/RuleInfo.lean
@@ -10,6 +10,7 @@ public import Aesop.Forward.SlotIndex
 public import Aesop.RulePattern
 public import Aesop.Util.Basic
 public import Aesop.Util.UnionFind
+public import Batteries.Data.Array.Basic
 
 public section
 

diff --git a/Aesop/Frontend/Basic.lean b/Aesop/Frontend/Basic.lean
@@ -5,7 +5,9 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Lean
+import Lean
+public import Lean.Exception
+public import Lean.Elab.Exception
 
 public section
 

diff --git a/Aesop/Frontend/Command.lean b/Aesop/Frontend/Command.lean
@@ -78,7 +78,7 @@ elab_rules : command
 
 def evalStatsReport? (name : Name) : CoreM (Option StatsReport) := do
   try
-    unsafe evalConstCheck StatsReport ``StatsReport name
+    unsafe some <$> evalConstCheck StatsReport ``StatsReport name
   catch _ =>
     return none
 

diff --git a/Aesop/Frontend/Tactic.lean b/Aesop/Frontend/Tactic.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 module
 
+import Lean
 public import Aesop.Frontend.RuleExpr
 public import Aesop.Options
 public import Batteries.Linter.UnreachableTactic

diff --git a/Aesop/Index.lean b/Aesop/Index.lean
@@ -12,8 +12,8 @@ public import Aesop.RulePattern
 public import Aesop.Rule.Basic
 public import Aesop.Tracing
 public import Batteries.Lean.Meta.InstantiateMVars
-public import Batteries.Lean.PersistentHashSet
-public import Batteries.Lean.Meta.DiscrTree
+import Batteries.Lean.PersistentHashSet
+import Batteries.Lean.Meta.DiscrTree
 
 public section
 

diff --git a/Aesop/Index/DiscrTreeConfig.lean b/Aesop/Index/DiscrTreeConfig.lean
@@ -5,7 +5,9 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Lean
+import Lean
+public import Lean.Meta.Basic
+public import Lean.Meta.DiscrTree.Types
 
 public section
 

diff --git a/Aesop/Index/Forward.lean b/Aesop/Index/Forward.lean
@@ -8,7 +8,7 @@ module
 public import Aesop.Forward.Match.Types
 public import Aesop.Rule.Forward
 public import Aesop.Index.Basic
-public import Batteries.Lean.Meta.DiscrTree
+import Batteries.Lean.Meta.DiscrTree
 
 public section
 

diff --git a/Aesop/Index/RulePattern.lean b/Aesop/Index/RulePattern.lean
@@ -8,7 +8,7 @@ module
 public import Aesop.Index.Basic
 public import Aesop.Util.OrderedHashSet
 public import Aesop.RuleTac.GoalDiff
-public import Batteries.Lean.Meta.DiscrTree
+import Batteries.Lean.Meta.DiscrTree
 
 public section
 

diff --git a/Aesop/Options/Public.lean b/Aesop/Options/Public.lean
@@ -1,6 +1,7 @@
 module
 
-public import Lean
+import Lean
+public import Lean.Data.Options
 
 public section
 

diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean
@@ -10,6 +10,8 @@ public import Aesop.Index.Forward
 public import Aesop.RuleSet.Filter
 public import Aesop.RuleSet.Member
 public import Aesop.Tree.Data.ForwardRuleMatches
+import Batteries.Lean.PersistentHashMap
+import Batteries.Lean.PersistentHashSet
 
 public section
 

diff --git a/Aesop/RuleSet/Name.lean b/Aesop/RuleSet/Name.lean
@@ -5,7 +5,7 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Lean
+import Lean
 
 public section
 

diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean
@@ -13,7 +13,6 @@ public import Aesop.RuleTac.GoalDiff
 public import Aesop.RuleTac.FVarIdSubst
 public import Aesop.Script.CtorNames
 public import Aesop.Script.Step
-public import Batteries.Lean.Meta.SavedState
 public import Aesop.Options.Internal
 
 public section

diff --git a/Aesop/RuleTac/ElabRuleTerm.lean b/Aesop/RuleTac/ElabRuleTerm.lean
@@ -5,6 +5,10 @@ Authors: Jannis Limperg
 -/
 module
 
+import Lean
+public import Lean.Elab.Tactic.Basic
+public import Lean.Meta.Tactic.Simp.Types
+public import Lean.Meta.Tactic.Simp.Simproc
 public import Aesop.ElabM
 
 public section

diff --git a/Aesop/RuleTac/FVarIdSubst.lean b/Aesop/RuleTac/FVarIdSubst.lean
@@ -5,7 +5,9 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Lean
+import Lean
+public import Std.Data.HashMap.Basic
+public import Lean.Meta.Tactic.FVarSubst
 
 public section
 

diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean
@@ -5,12 +5,13 @@ Authors: Jannis Limperg
 -/
 module
 
+import Lean
 public import Aesop.Forward.Match
 public import Aesop.RuleTac.Basic
 public import Aesop.RuleTac.ElabRuleTerm
 public import Aesop.RuleTac.Forward.Basic
 public import Aesop.Script.SpecificTactics
-public import Batteries.Lean.Meta.UnusedNames
+import Batteries.Lean.Meta.UnusedNames
 
 public section
 

diff --git a/Aesop/RuleTac/Forward/Basic.lean b/Aesop/RuleTac/Forward/Basic.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 module
 
+import Lean
 public import Aesop.Util.Basic
 public import Aesop.Util.EqualUpToIds
 

diff --git a/Aesop/Saturate.lean b/Aesop/Saturate.lean
@@ -11,7 +11,7 @@ public import Aesop.RuleSet
 public import Aesop.RuleTac
 public import Aesop.Search.Expansion.Basic
 public import Aesop.Script.Check
-public import Batteries.Data.BinomialHeap.Basic
+import Batteries.Data.BinomialHeap.Basic
 
 public section
 
@@ -124,7 +124,7 @@ where
 
 namespace Stateful
 
-abbrev Queue := BinomialHeap ForwardRuleMatch ForwardRuleMatch.le
+private abbrev Queue := BinomialHeap ForwardRuleMatch ForwardRuleMatch.le
 
 partial def saturateCore (rs : LocalRuleSet) (goal : MVarId) : SaturateM MVarId :=
   withExceptionPrefix "saturate: internal error: " do

diff --git a/Aesop/Script/CtorNames.lean b/Aesop/Script/CtorNames.lean
@@ -1,5 +1,6 @@
 module
 
+public import Lean.Meta.Tactic.Induction
 public import Aesop.Util.Basic
 
 public section

diff --git a/Aesop/Script/GoalWithMVars.lean b/Aesop/Script/GoalWithMVars.lean
@@ -1,6 +1,7 @@
 module
 
-public import Lean
+import Lean
+public import Lean.Meta.Basic
 
 public section
 

diff --git a/Aesop/Script/Main.lean b/Aesop/Script/Main.lean
@@ -11,6 +11,7 @@ public import Aesop.Script.StructureStatic
 public import Aesop.Script.OptimizeSyntax
 public import Aesop.Stats.Basic
 public import Aesop.Options.Internal
+import Batteries.Lean.Meta.SavedState
 
 public section
 

diff --git a/Aesop/Script/OptimizeSyntax.lean b/Aesop/Script/OptimizeSyntax.lean
@@ -5,7 +5,8 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Lean
+import Lean
+public import Std.Data.HashSet.Basic
 
 public section
 

diff --git a/Aesop/Script/SScript.lean b/Aesop/Script/SScript.lean
@@ -1,6 +1,7 @@
 module
 
 public import Aesop.Script.Step
+import Batteries.Tactic.PermuteGoals
 
 public section
 

diff --git a/Aesop/Script/SpecificTactics.lean b/Aesop/Script/SpecificTactics.lean
@@ -5,13 +5,15 @@ Authors: Jannis Limperg
 -/
 module
 
+import Lean
+public import Lean.Meta.Tactic.Cases
 public import Aesop.Util.Tactic
 public import Aesop.Util.Tactic.Ext
 public import Aesop.Util.Tactic.Unfold
 public import Aesop.Util.Unfold
 public import Aesop.Script.CtorNames
 public import Aesop.Script.ScriptM
-public import Batteries.Lean.Meta.Inaccessible
+import Batteries.Lean.Meta.Inaccessible
 
 public section
 

diff --git a/Aesop/Script/Step.lean b/Aesop/Script/Step.lean
@@ -10,7 +10,8 @@ public import Aesop.Script.Tactic
 public import Aesop.Script.TacticState
 public import Aesop.Script.Util
 public import Aesop.Tracing
-public import Batteries.Tactic.PermuteGoals
+import Batteries.Tactic.PermuteGoals
+import Batteries.Lean.Meta.SavedState
 
 public section
 

diff --git a/Aesop/Script/StructureDynamic.lean b/Aesop/Script/StructureDynamic.lean
@@ -10,6 +10,7 @@ public import Aesop.Script.UScriptToSScript
 public import Aesop.Script.Util
 public import Aesop.Script.SScript
 public import Aesop.Tracing
+import Batteries.Lean.Meta.SavedState
 
 public section
 

diff --git a/Aesop/Script/Tactic.lean b/Aesop/Script/Tactic.lean
@@ -5,7 +5,8 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Lean
+import Lean
+public import Lean.Meta.Basic
 
 public section
 

diff --git a/Aesop/Script/TacticState.lean b/Aesop/Script/TacticState.lean
@@ -5,7 +5,8 @@ Authors: Jannis Limperg
 -/
 module
 
-public import Batteries.Lean.Meta.Basic
+import Lean
+import Batteries.Lean.Meta.Basic
 public import Aesop.Script.GoalWithMVars
 
 public section

diff --git a/Aesop/Script/UScript.lean b/Aesop/Script/UScript.lean
@@ -6,6 +6,7 @@ Authors: Jannis Limperg
 module
 
 public import Aesop.Script.Step
+import Batteries.Lean.Meta.SavedState
 
 public section
 

diff --git a/Aesop/Script/Util.lean b/Aesop/Script/Util.lean
@@ -7,7 +7,7 @@ module
 
 public import Aesop.Util.Basic
 public import Aesop.Util.EqualUpToIds
-public import Batteries.Lean.Meta.SavedState
+import Batteries.Lean.Meta.SavedState
 
 public section
 

diff --git a/Aesop/Search/Expansion/Norm.lean b/Aesop/Search/Expansion/Norm.lean
@@ -14,7 +14,8 @@ public import Aesop.Search.Expansion.Simp
 public import Aesop.Search.RuleSelection
 public import Aesop.Search.SearchM
 public import Aesop.Tree.State
-public import Batteries.Lean.HashSet
+import Batteries.Lean.HashSet
+public import Batteries.Lean.Meta.SavedState
 
 public section
 

diff --git a/Aesop/Tracing.lean b/Aesop/Tracing.lean
@@ -6,7 +6,6 @@ Authors: Jannis Limperg
 module
 
 public import Aesop.Util.Basic
-public import Batteries.Data.Array.Basic
 public import Lean.Elab.Term
 public import Lean.Meta.Tactic.Simp
 
@@ -110,7 +109,7 @@ macro "aesop_trace![" opt:ident "] " msg:(interpolatedStr(term) <|> term) :
   `(doElem| Lean.addTrace (Aesop.TraceOption.traceClass $opt) $msg)
 
 macro "aesop_trace[" opt:ident "] "
-    msg:(interpolatedStr(term) <|> Parser.Term.do <|> term) : doElem => do
+    msg:(interpolatedStr(term) <|> term) : doElem => do
   let msg := msg.raw
   let opt ← mkIdent <$> resolveTraceOption opt
   match msg with

diff --git a/Aesop/Tree/AddRapp.lean b/Aesop/Tree/AddRapp.lean
@@ -10,6 +10,7 @@ public import Aesop.Forward.State.ApplyGoalDiff
 public import Aesop.Tree.Traversal
 public import Aesop.Tree.TreeM
 public import Aesop.Util.UnionFind
+import Batteries.Lean.Meta.SavedState
 
 public section
-Original file line number
+Diff line change
@@ Expand Up / @@ -6,6 +6,7 @@ Authors: Jannis Limperg @@
     module
     public import Aesop.Builder.Basic
+    import Batteries.Lean.Expr
     public section
@@ Expand Down @@