structure Aesop.Script.DynStructureM.Context : Type

• steps : Lean.PHashMap Lean.MVarId (Nat × Aesop.Script.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 Aesop.Script.DynStructureM.Context

Equations

• Aesop.Script.DynStructureM.instInhabitedContext = { default := { steps := default } }

structure Aesop.Script.DynStructureM.State : Type

• perfect : Bool

def Aesop.Script.DynStructureM.Context.updateMVarIds (c : Aesop.Script.DynStructureM.Context) (map : Lean.HashMap Lean.MVarId Lean.MVarId) : Aesop.Script.DynStructureM.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.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Equations

• Aesop.Script.DynStructureM = ReaderT Aesop.Script.DynStructureM.Context (StateRefT' IO.RealWorld Aesop.Script.DynStructureM.State Lean.MetaM)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

structure Aesop.Script.DynStructureResult : Type

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.