Documentation

Aesop.Tree.UnsafeQueue

structure Aesop.PostponedSafeRule :

rule : Aesop.SafeRule
output : Aesop.RuleTacOutput

Instances For

Aesop.instInhabitedPostponedSafeRule

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 :

unsafeRule: Aesop.IndexMatchResult Aesop.UnsafeRule → Aesop.UnsafeQueueEntry
postponedSafeRule: Aesop.PostponedSafeRule → Aesop.UnsafeQueueEntry

Instances For

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 :

Equations

Aesop.UnsafeQueue = Subarray Aesop.UnsafeQueueEntry

Instances For

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)