- empty: Aesop.Script.StepTree
- node: Aesop.Script.Step → Nat → Array Aesop.Script.StepTree → Aesop.Script.StepTree
Instances For
Equations
- t.toMessageData = t.toMessageData?.getD ((Lean.MessageData.ofFormat ∘ Std.format) "empty")
Instances For
Equations
- Aesop.Script.instToMessageDataStepTree = { toMessageData := Aesop.Script.StepTree.toMessageData }
Equations
- One or more equations did not get rendered due to their size.
Instances For
partial def
Aesop.Script.UScript.toStepTree.go
(m : Lean.HashMap Lean.MVarId (Nat × Aesop.Script.Step))
(goal : Lean.MVarId)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- t.focusableGoals = (runST fun (x : Type) => (Aesop.Script.StepTree.focusableGoals.go t).run ∅).snd
Instances For
partial def
Aesop.Script.StepTree.focusableGoals.go
{σ : Type}
:
Aesop.Script.StepTree → StateRefT' σ (Lean.HashMap Lean.MVarId Nat) (ST σ) (Array Nat)
Equations
- t.numSiblings = (runST fun (x : Type) => (Aesop.Script.StepTree.numSiblings.go 0 t).run ∅).snd
Instances For
partial def
Aesop.Script.StepTree.numSiblings.go
{σ : Type}
(parentNumGoals : Nat)
:
Aesop.Script.StepTree → StateRefT' σ (Lean.HashMap Lean.MVarId Nat) (ST σ) Unit
def
Aesop.Script.orderedUScriptToSScript
(uscript : Aesop.Script.UScript)
(tacticState : Aesop.Script.TacticState)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
partial def
Aesop.Script.orderedUScriptToSScript.go
(uscript : Aesop.Script.UScript)
(focusable : Lean.HashMap Lean.MVarId Nat)
(numSiblings : Lean.HashMap Lean.MVarId Nat)
(start : Nat)
(stop : Nat)
(tacticState : Aesop.Script.TacticState)
: