inductive Aesop.Script.StepTree : Type

• empty: Aesop.Script.StepTree
• node: Aesop.Script.Step → Nat → Array Aesop.Script.StepTree → Aesop.Script.StepTree

Instances For

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

instance Aesop.Script.instNonemptyStepTree : Nonempty Aesop.Script.StepTree

Equations

• Aesop.Script.instNonemptyStepTree = ⋯

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

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

Equations

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

instance Aesop.Script.instToMessageDataStepTree : Lean.ToMessageData Aesop.Script.StepTree

Equations

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

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

Equations

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

partial def Aesop.Script.UScript.toStepTree.go (m : Lean.HashMap Lean.MVarId (Nat × Aesop.Script.Step)) (goal : Lean.MVarId) : Aesop.Script.StepTree

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

Equations

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

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 : Aesop.Script.StepTree) : Lean.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} : Aesop.Script.StepTree → StateRefT' σ (Lean.HashMap Lean.MVarId Nat) (ST σ) (Array Nat)

def Aesop.Script.StepTree.numSiblings (t : Aesop.Script.StepTree) : Lean.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) : Aesop.Script.StepTree → StateRefT' σ (Lean.HashMap Lean.MVarId Nat) (ST σ) Unit

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

Equations

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

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) : Lean.CoreM (Aesop.Script.SScript × Aesop.Script.TacticState)