structure Aesop.PostponedSafeRule : Type

• rule : SafeRule
• output : RuleTacOutput

instance Aesop.instInhabitedPostponedSafeRule : Inhabited PostponedSafeRule

Equations

• Aesop.instInhabitedPostponedSafeRule = { default := { rule := default, output := default } }

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

Equations

• One or more equations did not get rendered due to their size.

inductive Aesop.UnsafeQueueEntry : Type

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

instance Aesop.instInhabitedUnsafeQueueEntry : Inhabited UnsafeQueueEntry

Equations

• Aesop.instInhabitedUnsafeQueueEntry = { default := Aesop.UnsafeQueueEntry.unsafeRule default }

instance Aesop.UnsafeQueueEntry.instToString : ToString UnsafeQueueEntry

Equations

• One or more equations did not get rendered due to their size.

def Aesop.UnsafeQueueEntry.successProbability : UnsafeQueueEntry → Percent

Equations

• (Aesop.UnsafeQueueEntry.unsafeRule r).successProbability = r.rule.extra.successProbability
• (Aesop.UnsafeQueueEntry.postponedSafeRule r).successProbability = Aesop.postponedSafeRuleSuccessProbability

def Aesop.UnsafeQueueEntry.name : UnsafeQueueEntry → RuleName

Equations

• (Aesop.UnsafeQueueEntry.unsafeRule r).name = r.rule.name
• (Aesop.UnsafeQueueEntry.postponedSafeRule r).name = r.rule.name

instance Aesop.UnsafeQueueEntry.instOrd : Ord UnsafeQueueEntry

Equations

• One or more equations did not get rendered due to their size.

def Aesop.UnsafeQueue : Type

Equations

• Aesop.UnsafeQueue = Subarray Aesop.UnsafeQueueEntry

instance Aesop.UnsafeQueue.instEmptyCollection : EmptyCollection UnsafeQueue

Equations

• Aesop.UnsafeQueue.instEmptyCollection = inferInstanceAs (EmptyCollection (Subarray Aesop.UnsafeQueueEntry))

instance Aesop.UnsafeQueue.instInhabited : Inhabited UnsafeQueue

Equations

• Aesop.UnsafeQueue.instInhabited = inferInstanceAs (Inhabited (Subarray Aesop.UnsafeQueueEntry))

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• q.entriesToMessageData = Array.map Lean.toMessageData (Subarray.toArray q)