source
inductive Aesop.Script.StepTree :
Type

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

Instances For

source
instance Aesop.Script.instNonemptyStepTree :
Nonempty StepTree
source
partial def Aesop.Script.StepTree.toMessageData? :
StepTree → Option Lean.MessageData
source
def Aesop.Script.StepTree.toMessageData (t : StepTree) :
Lean.MessageData
Equations

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

Instances For

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

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

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

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

Instances For

source
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

Instances For

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

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

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For