structure Aesop.PostponedSafeRule : Type

• rule : SafeRule
• output : RuleTacOutput

instance Aesop.instInhabitedPostponedSafeRule : Inhabited PostponedSafeRule

def Aesop.PostponedSafeRule.toUnsafeRule (r : PostponedSafeRule) : UnsafeRule

inductive Aesop.UnsafeQueueEntry : Type

• unsafeRule (r : IndexMatchResult UnsafeRule) : UnsafeQueueEntry
• postponedSafeRule (r : PostponedSafeRule) : UnsafeQueueEntry

instance Aesop.instInhabitedUnsafeQueueEntry : Inhabited UnsafeQueueEntry

instance Aesop.UnsafeQueueEntry.instToString : ToString UnsafeQueueEntry

def Aesop.UnsafeQueueEntry.successProbability : UnsafeQueueEntry → Percent

def Aesop.UnsafeQueueEntry.name : UnsafeQueueEntry → RuleName

instance Aesop.UnsafeQueueEntry.instOrd : Ord UnsafeQueueEntry

def Aesop.UnsafeQueue : Type

instance Aesop.UnsafeQueue.instEmptyCollection : EmptyCollection UnsafeQueue

instance Aesop.UnsafeQueue.instInhabited : Inhabited UnsafeQueue

def Aesop.UnsafeQueue.initial (postponedSafeRules : Array PostponedSafeRule) (unsafeRules : Array (IndexMatchResult UnsafeRule)) : UnsafeQueue

def Aesop.UnsafeQueue.entriesToMessageData (q : UnsafeQueue) : Array Lean.MessageData