← Mathematical handbook

opaque Aesop.safeExpansionFailedExceptionId : Lean.InternalExceptionId

def Aesop.isSafeExpansionFailedException : Lean.Exception → Bool

Equations

• Aesop.isSafeExpansionFailedException (Lean.Exception.internal id extra) = (id == Aesop.safeExpansionFailedExceptionId)
• Aesop.isSafeExpansionFailedException x✝ = false

def Aesop.safeExpansionFailedException : Lean.Exception

Equations

• Aesop.safeExpansionFailedException = Lean.Exception.internal Aesop.safeExpansionFailedExceptionId

structure Aesop.SafeExpansionM.State : Type

• numRapps : Nat

@[reducible, inline]

abbrev Aesop.SafeExpansionM (Q : Type) [Queue Q] (α : Type) : Type

Equations

• Aesop.SafeExpansionM Q = StateRefT' IO.RealWorld Aesop.SafeExpansionM.State (Aesop.SearchM Q)

def Aesop.expandSafePrefix {Q : Type} [Queue Q] : SearchM Q Bool

Equations

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