Aesop.Rule.Forward

source

inductive Aesop.ForwardRulePriority :

Type

The priority of a forward rule.

normSafe (n : Int) : ForwardRulePriority
If the rule is a norm or safe rule, its priority is an integer.
unsafe (p : Percent) : ForwardRulePriority
If the rule is an unsafe rule, its priority is a percentage representing the rule's success probability.

Instances For

source

@[implicit_reducible]

instance Aesop.instInhabitedForwardRulePriority :

Inhabited ForwardRulePriority

source

def Aesop.instInhabitedForwardRulePriority.default :

ForwardRulePriority

Instances For

source

@[implicit_reducible]

instance Aesop.instBEqForwardRulePriority :

BEq ForwardRulePriority

source

def Aesop.instBEqForwardRulePriority.beq :

ForwardRulePriority → ForwardRulePriority → Bool

Instances For

source

def Aesop.ForwardRulePriority.penalty? :

ForwardRulePriority → Option Int

If a ForwardRulePriority contains a penalty, extract it.

Instances For

source

def Aesop.ForwardRulePriority.successProbability? :

ForwardRulePriority → Option Percent

If a ForwardRulePriority contains a success probability, extract it.

Instances For

source

def Aesop.ForwardRulePriority.compare (p₁ p₂ : ForwardRulePriority) :

Ordering

Compare two rule priorities. Less means higher priority ('better'). Norm/safe rules have higher priority than unsafe rules. Among norm/safe rules, lower penalty is better. Among unsafe rules, higher percentage is better.

Instances For

source

@[implicit_reducible]

instance Aesop.ForwardRulePriority.instOrd :

Ord ForwardRulePriority

source

@[implicit_reducible]

instance Aesop.ForwardRulePriority.instToString :

ToString ForwardRulePriority

source

structure Aesop.ForwardRuleextends Aesop.ForwardRuleInfo :

Type