- 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 currentMetaM
state. This state evolves during dynamic structuring and we continually update thesteps
so that this map's keys refer to metavariables which exist in the currentMetaM
state.
Instances For
Equations
- Aesop.Script.DynStructureM.instInhabitedContext = { default := { steps := default } }
def
Aesop.Script.DynStructureM.Context.updateMVarIds
(c : Context)
(map : Std.HashMap Lean.MVarId Lean.MVarId)
:
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.
@[reducible, inline]
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.
def
Aesop.Script.withUpdatedMVarIds
{α : Type}
(oldPostState newPostState : Lean.Meta.SavedState)
(oldPostGoals newPostGoals : Array Lean.MVarId)
(onFailure onSuccess : DynStructureM α)
:
Equations
- One or more equations did not get rendered due to their size.
- postState : Lean.Meta.SavedState
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.
partial def
Aesop.Script.structureDynamicCore.go
(preGoal : Lean.MVarId)
(preState : Lean.Meta.SavedState)
(preGoals : Array Lean.MVarId)
:
partial def
Aesop.Script.structureDynamicCore.goStructured
(preGoal : Lean.MVarId)
(preState : Lean.Meta.SavedState)
(preGoals : Array Lean.MVarId)
(firstPreGoal : Lean.MVarId)
:
partial def
Aesop.Script.structureDynamicCore.goUnstructured
(preGoal : Lean.MVarId)
(preState : Lean.Meta.SavedState)
(preGoals : Array Lean.MVarId)
:
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))
Equations
- One or more equations did not get rendered due to their size.