inductive Aesop.Script.StepTree : Type

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

Instances For

• Aesop.Script.instNonemptyStepTree
• Aesop.Script.instToMessageDataStepTree

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.

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 α

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

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

Equations

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

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

Equations

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

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