structure Aesop.PostponedSafeRule : Type

• rule : Aesop.SafeRule
• output : Aesop.RuleTacOutput

instance Aesop.instInhabitedPostponedSafeRule : Inhabited Aesop.PostponedSafeRule

Equations

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

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

Equations

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

inductive Aesop.UnsafeQueueEntry : Type

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

instance Aesop.instInhabitedUnsafeQueueEntry : Inhabited Aesop.UnsafeQueueEntry

Equations

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

instance Aesop.UnsafeQueueEntry.instToString : ToString Aesop.UnsafeQueueEntry

Equations

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

def Aesop.UnsafeQueueEntry.successProbability : Aesop.UnsafeQueueEntry → Aesop.Percent

Equations

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

def Aesop.UnsafeQueueEntry.name : Aesop.UnsafeQueueEntry → Aesop.RuleName

Equations

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

instance Aesop.UnsafeQueueEntry.instOrd : Ord Aesop.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 Aesop.UnsafeQueue

Equations

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

instance Aesop.UnsafeQueue.instInhabited : Inhabited Aesop.UnsafeQueue

Equations

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

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

Equations

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

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

Equations

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