Documentation

Aesop.Tree.UnsafeQueue

source
structure Aesop.PostponedSafeRule :
Type
Instances For
    source
    @[instance_reducible]
    instance Aesop.instInhabitedPostponedSafeRule :
    Inhabited PostponedSafeRule
    source
    def Aesop.PostponedSafeRule.toUnsafeRule (r : PostponedSafeRule) :
    UnsafeRule
    Instances For
      source
      inductive Aesop.UnsafeQueueEntry :
      Type
      Instances For
        source
        @[instance_reducible]
        instance Aesop.instInhabitedUnsafeQueueEntry :
        Inhabited UnsafeQueueEntry
        source
        @[instance_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
            @[instance_reducible]
            instance Aesop.UnsafeQueueEntry.instOrd :
            Ord UnsafeQueueEntry
            source
            def Aesop.UnsafeQueue :
            Type
            Instances For
              source
              @[instance_reducible]
              instance Aesop.UnsafeQueue.instEmptyCollection :
              EmptyCollection UnsafeQueue
              source
              @[instance_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