inductive Aesop.Script.StepTree : Type

• empty : StepTree
• node (step : Step) (index : Nat) (children : Array StepTree) : StepTree

instance Aesop.Script.instNonemptyStepTree : Nonempty StepTree

partial def Aesop.Script.StepTree.toMessageData? : StepTree → Option Lean.MessageData

def Aesop.Script.StepTree.toMessageData (t : StepTree) : Lean.MessageData

Equations

• t.toMessageData = t.toMessageData?.getD ((Lean.MessageData.ofFormat ∘ Std.format) "empty")

instance Aesop.Script.instToMessageDataStepTree : Lean.ToMessageData StepTree

Equations

• Aesop.Script.instToMessageDataStepTree = { toMessageData := Aesop.Script.StepTree.toMessageData }

def Aesop.Script.UScript.toStepTree (s : UScript) : StepTree

Equations

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

def Aesop.Script.sortDedupArrays {α : Type u_1} [Ord α] (as : Array (Array α)) : Array α

Equations

• Aesop.Script.sortDedupArrays as = (Array.foldl (fun (x1 x2 : Array α) => x1 ++ x2) (Array.mkEmpty (Array.foldl (fun (x1 : Nat) (x2 : Array α) => x1 + x2.size) 0 as)) as).sortDedup

def Aesop.Script.isConsecutiveSequence (ns : Array Nat) : Bool

Equations

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

def Aesop.Script.StepTree.focusableGoals (t : StepTree) : Std.HashMap Lean.MVarId Nat

Equations

• t.focusableGoals = (runST fun (x : Type) => (Aesop.Script.StepTree.focusableGoals.go✝ t).run ∅).snd

def Aesop.Script.StepTree.numSiblings (t : StepTree) : Std.HashMap Lean.MVarId Nat

Equations

• t.numSiblings = (runST fun (x : Type) => (Aesop.Script.StepTree.numSiblings.go✝ 0 t).run ∅).snd

def Aesop.Script.orderedUScriptToSScript (uscript : UScript) (tacticState : TacticState) : Lean.CoreM SScript

Equations

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