class Aesop.Queue (Q : Type) : Type

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

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

Equations

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