Documentation

Aesop.Search.ExpandSafePrefix

source
def Aesop.safeExpansionFailedException :
Lean.Exception
Equations
    Instances For
      source
      def Aesop.isSafeExpansionFailedException :
      Lean.Exception → Bool
      Equations
        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
            Equations
              Instances For
                source
                def Aesop.expandSafePrefix {Q : Type} [Queue Q] :
                SearchM Q Bool
                Equations
                  Instances For