source
structure Aesop.PostponedSafeRule :
Type

- rule : SafeRule
- output : RuleTacOutput

Instances For

source
instance Aesop.instInhabitedPostponedSafeRule :
Inhabited PostponedSafeRule
Equations

- Aesop.instInhabitedPostponedSafeRule = { default := Aesop.instInhabitedPostponedSafeRule.default }

source
def Aesop.instInhabitedPostponedSafeRule.default :
PostponedSafeRule
Equations

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

Instances For

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

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

Instances For

source
inductive Aesop.UnsafeQueueEntry :
Type

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

Instances For

source
def Aesop.instInhabitedUnsafeQueueEntry.default :
UnsafeQueueEntry
Equations

- Aesop.instInhabitedUnsafeQueueEntry.default = Aesop.UnsafeQueueEntry.unsafeRule default

Instances For

source
instance Aesop.instInhabitedUnsafeQueueEntry :
Inhabited UnsafeQueueEntry
Equations

- Aesop.instInhabitedUnsafeQueueEntry = { default := Aesop.instInhabitedUnsafeQueueEntry.default }

source
instance Aesop.UnsafeQueueEntry.instToString :
ToString UnsafeQueueEntry
Equations

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

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

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

Instances For

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

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

Instances For

source
instance Aesop.UnsafeQueueEntry.instOrd :
Ord UnsafeQueueEntry
Equations

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

source
def Aesop.UnsafeQueue :
Type
Equations

- Aesop.UnsafeQueue = Subarray Aesop.UnsafeQueueEntry

Instances For

source
instance Aesop.UnsafeQueue.instEmptyCollection :
EmptyCollection UnsafeQueue
Equations

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

source
instance Aesop.UnsafeQueue.instInhabited :
Inhabited UnsafeQueue
Equations

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

source
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.

Instances For

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

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

Instances For