structure Aesop.Script.StaticStructureM.State : Type

• perfect : Bool

structure Aesop.Script.StaticStructureM.Context : Type

• steps : Std.HashMap Lean.MVarId (Nat × Step)

@[reducible, inline]

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

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

def Aesop.Script.structureStaticCore (tacticState : TacticState) (script : UScript) : Lean.CoreM (UScript × Bool)

def Aesop.Script.UScript.toSScriptStatic (tacticState : TacticState) (uscript : UScript) : Lean.CoreM (SScript × Bool)