def Aesop.isSafeExpansionFailedException : Lean.Exception → Bool

Equations

• Aesop.isSafeExpansionFailedException x = match x with | Lean.Exception.internal id extra => id == Aesop.safeExpansionFailedExceptionId | x => false

def Aesop.safeExpansionFailedException : Lean.Exception

Equations

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

opaque Aesop.safeExpansionFailedExceptionId : Lean.InternalExceptionId

structure Aesop.SafeExpansionM.State : Type

• numRapps : Nat

@[inline, reducible]

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

Equations

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

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

Equations

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