source
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.

Instances For

source
def Aesop.Script.DynStructureM.instInhabitedContext.default :
Context
Equations

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

Instances For

source
instance Aesop.Script.DynStructureM.instInhabitedContext :
Inhabited Context
Equations

- Aesop.Script.DynStructureM.instInhabitedContext = { default := Aesop.Script.DynStructureM.instInhabitedContext.default }

source
structure Aesop.Script.DynStructureM.State :
Type

- perfect : Bool

Instances For

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

Given a bijective map `map` from new `MVarId`s to old `MVarId`s, 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.

Instances For

source
@[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)

Instances For

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

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

Instances For

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

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

Instances For

source
structure Aesop.Script.DynStructureResult :
Type

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

Instances For

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

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

Instances For

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

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

Instances For