- steps : Std.HashMap Lean.MVarId (Nat × Step)
Instances For
@[reducible, inline]
Equations
Instances For
def
Aesop.Script.StaticStructureM.run
{α : Type}
(script : UScript)
(x : StaticStructureM α)
:
Lean.CoreM (α × Bool)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.Script.structureStaticCore.nextStep
(tacticState : TacticState)
(mainGoal : GoalWithMVars)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.