structure Aesop.BestFirstQueue.ActiveGoal : Type

• goal : GoalRef
• priority : Percent
• lastExpandedInIteration : Iteration
• addedInIteration : Iteration

def Aesop.BestFirstQueue.ActiveGoal.le (g h : ActiveGoal) : Bool

Equations

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

def Aesop.BestFirstQueue.ActiveGoal.ofGoalRef (gref : GoalRef) : BaseIO ActiveGoal

Equations

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

def Aesop.BestFirstQueue : Type

Equations

• Aesop.BestFirstQueue = Batteries.BinomialHeap Aesop.BestFirstQueue.ActiveGoal Aesop.BestFirstQueue.ActiveGoal.le

def Aesop.BestFirstQueue.init : BestFirstQueue

Equations

• Aesop.BestFirstQueue.init = Batteries.BinomialHeap.empty

def Aesop.BestFirstQueue.addGoals (q : BestFirstQueue) (grefs : Array GoalRef) : BaseIO BestFirstQueue

Equations

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

def Aesop.BestFirstQueue.popGoal (q : BestFirstQueue) : Option GoalRef × BestFirstQueue

Equations

• q.popGoal = match Batteries.BinomialHeap.deleteMin q with | none => (none, q) | some (ag, q) => (some ag.goal, q)

@[implicit_reducible]

instance Aesop.instQueueBestFirstQueue : Queue BestFirstQueue

Equations

• Aesop.instQueueBestFirstQueue = { init := pure Aesop.BestFirstQueue.init, addGoals := Aesop.BestFirstQueue.addGoals, popGoal := fun (q : Aesop.BestFirstQueue) => pure q.popGoal }

structure Aesop.LIFOQueue : Type

• goals : Array GoalRef

def Aesop.LIFOQueue.init : LIFOQueue

Equations

• Aesop.LIFOQueue.init = { goals := #[] }

def Aesop.LIFOQueue.addGoals (q : LIFOQueue) (grefs : Array GoalRef) : LIFOQueue

Equations

• q.addGoals grefs = { goals := q.goals ++ grefs.reverse }

def Aesop.LIFOQueue.popGoal (q : LIFOQueue) : Option GoalRef × LIFOQueue

Equations

• q.popGoal = match q.goals.back? with | some g => (some g, { goals := q.goals.pop }) | none => (none, q)

@[implicit_reducible]

instance Aesop.LIFOQueue.instQueue : Queue LIFOQueue

Equations

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

structure Aesop.FIFOQueue : Type

• goals : Array GoalRef
• pos : Nat

def Aesop.FIFOQueue.init : FIFOQueue

Equations

• Aesop.FIFOQueue.init = { goals := #[], pos := 0 }

def Aesop.FIFOQueue.addGoals (q : FIFOQueue) (grefs : Array GoalRef) : FIFOQueue

Equations

• q.addGoals grefs = { goals := q.goals ++ grefs, pos := q.pos }

def Aesop.FIFOQueue.popGoal (q : FIFOQueue) : Option GoalRef × FIFOQueue

Equations

• q.popGoal = if h : q.pos < q.goals.size then (some q.goals[q.pos], { goals := q.goals, pos := q.pos + 1 }) else (none, q)

@[implicit_reducible]

instance Aesop.FIFOQueue.instQueue : Queue FIFOQueue

Equations

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

def Aesop.Options.queue (opts : Options) : (Q : Type) × Queue Q

Equations

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