structure Aesop.Script.DynStructureM.Context : Type

• steps : Lean.PHashMap Lean.MVarId (Nat × Step)

  The tactic invocation steps corresponding to the original unstructured script, but with MVarId keys adjusted to fit the current MetaM state. This state evolves during dynamic structuring and we continually update the steps so that this map's keys refer to metavariables which exist in the current MetaM state.

instance Aesop.Script.DynStructureM.instInhabitedContext : Inhabited Context

structure Aesop.Script.DynStructureM.State : Type

• perfect : Bool

def Aesop.Script.DynStructureM.Context.updateMVarIds (c : Context) (map : Std.HashMap Lean.MVarId Lean.MVarId) : Context

Given a bijective map map from new MVarIds to old MVarIds, update the steps of the context c such that each entry whose key is an old MVarId m is replaced with an entry whose key is the corresponding new MVarId map⁻¹ m.

@[reducible, inline]

abbrev Aesop.Script.DynStructureM (α : Type) : Type

def Aesop.Script.DynStructureM.run {α : Type} (x : DynStructureM α) (script : UScript) : Lean.MetaM (α × Bool)

def Aesop.Script.withUpdatedMVarIds {α : Type} (oldPostState newPostState : Lean.Meta.SavedState) (oldPostGoals newPostGoals : Array Lean.MVarId) (onFailure onSuccess : DynStructureM α) : DynStructureM α

structure Aesop.Script.DynStructureResult : Type

• script : List Step
• postState : Lean.Meta.SavedState

def Aesop.Script.structureDynamicCore (preState : Lean.Meta.SavedState) (preGoal : Lean.MVarId) (uscript : UScript) : Lean.MetaM (Option (UScript × Bool))

partial def Aesop.Script.structureDynamicCore.go (preGoal : Lean.MVarId) (preState : Lean.Meta.SavedState) (preGoals : Array Lean.MVarId) : DynStructureM (Option DynStructureResult)

partial def Aesop.Script.structureDynamicCore.goStructured (preGoal : Lean.MVarId) (preState : Lean.Meta.SavedState) (preGoals : Array Lean.MVarId) (firstPreGoal : Lean.MVarId) : DynStructureM (Option DynStructureResult)

partial def Aesop.Script.structureDynamicCore.goUnstructured (preGoal : Lean.MVarId) (preState : Lean.Meta.SavedState) (preGoals : Array Lean.MVarId) : DynStructureM (Option DynStructureResult)

partial def Aesop.Script.structureDynamicCore.applyStepAndSolveRemaining (preGoal : Lean.MVarId) (preState : Lean.Meta.SavedState) (preGoals : Array Lean.MVarId) : Lean.MVarId → (goalPos : Nat) → (step : Step) → DynStructureM (Option DynStructureResult)

def Aesop.Script.UScript.toSScriptDynamic (preState : Lean.Meta.SavedState) (preGoal : Lean.MVarId) (uscript : UScript) : Lean.MetaM (Option (SScript × Bool))