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

partial def Aesop.Script.UScript.toStepTree.go (m : Std.HashMap Lean.MVarId (Nat × Step)) (goal : Lean.MVarId) : 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

partial def Aesop.Script.StepTree.focusableGoals.go {σ : Type} : StepTree → StateRefT' σ (Std.HashMap Lean.MVarId Nat) (ST σ) (Array Nat)

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

partial def Aesop.Script.StepTree.numSiblings.go {σ : Type} (parentNumGoals : Nat) : StepTree → StateRefT' σ (Std.HashMap Lean.MVarId Nat) (ST σ) Unit

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

partial def Aesop.Script.orderedUScriptToSScript.go (uscript : UScript) (focusable numSiblings : Std.HashMap Lean.MVarId Nat) (start stop : Nat) (tacticState : TacticState) : Lean.CoreM (SScript × TacticState)