class Aesop.Queue (Q : Type) : Type

• init : BaseIO Q
• addGoals : Q → Array GoalRef → BaseIO Q
• popGoal : Q → BaseIO (Option GoalRef × Q)

Instances

• Aesop.FIFOQueue.instQueue
• Aesop.LIFOQueue.instQueue
• Aesop.instQueueBestFirstQueue

def Aesop.Queue.init' {Q : Type} [Queue Q] (grefs : Array GoalRef) : BaseIO Q

Equations

• Aesop.Queue.init' grefs = do let __do_lift ← Aesop.Queue.init Aesop.Queue.addGoals __do_lift grefs