Documentation

Aesop.Search.ExpandSafePrefix

source
def Aesop.safeExpansionFailedException :
Lean.Exception
Instances For
    source
    def Aesop.isSafeExpansionFailedException :
    Lean.Exception → Bool
    Instances For
      source
      opaque Aesop.safeExpansionFailedExceptionId :
      Lean.InternalExceptionId
      source
      structure Aesop.SafeExpansionM.State :
      Type
      Instances For
        source
        @[reducible, inline]
        abbrev Aesop.SafeExpansionM (Q : Type) [Queue Q] (α : Type) :
        Type
        Instances For
          source
          def Aesop.expandSafePrefix {Q : Type} [Queue Q] :
          SearchM Q Bool
          Instances For