Documentation

Aesop.Tree.UnsafeQueue

source
structure Aesop.PostponedSafeRule :
Type
Instances For
    source
    def Aesop.instInhabitedPostponedSafeRule.default :
    PostponedSafeRule
    Instances For
      source
      @[implicit_reducible]
      instance Aesop.instInhabitedPostponedSafeRule :
      Inhabited PostponedSafeRule
      source
      def Aesop.PostponedSafeRule.toUnsafeRule (r : PostponedSafeRule) :
      UnsafeRule
      Instances For
        source
        inductive Aesop.UnsafeQueueEntry :
        Type
        Instances For
          source
          @[implicit_reducible]
          instance Aesop.instInhabitedUnsafeQueueEntry :
          Inhabited UnsafeQueueEntry
          source
          def Aesop.instInhabitedUnsafeQueueEntry.default :
          UnsafeQueueEntry
          Instances For
            source
            @[implicit_reducible]
            instance Aesop.UnsafeQueueEntry.instToString :
            ToString UnsafeQueueEntry
            source
            def Aesop.UnsafeQueueEntry.successProbability :
            UnsafeQueueEntry → Percent
            Instances For
              source
              def Aesop.UnsafeQueueEntry.name :
              UnsafeQueueEntry → RuleName
              Instances For
                source
                @[implicit_reducible]
                instance Aesop.UnsafeQueueEntry.instOrd :
                Ord UnsafeQueueEntry
                source
                def Aesop.UnsafeQueue :
                Type
                Instances For
                  source
                  @[implicit_reducible]
                  instance Aesop.UnsafeQueue.instEmptyCollection :
                  EmptyCollection UnsafeQueue
                  source
                  @[implicit_reducible]
                  instance Aesop.UnsafeQueue.instInhabited :
                  Inhabited UnsafeQueue
                  source
                  def Aesop.UnsafeQueue.initial (postponedSafeRules : Array PostponedSafeRule) (unsafeRules : Array (IndexMatchResult UnsafeRule)) :
                  UnsafeQueue
                  Instances For
                    source
                    def Aesop.UnsafeQueue.entriesToMessageData (q : UnsafeQueue) :
                    Array Lean.MessageData
                    Instances For