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

instance Aesop.Script.instToMessageDataStepTree : Lean.ToMessageData StepTree

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

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

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

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

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

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