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
def Aesop.instInhabitedForwardRulePriority.default :
ForwardRulePriority
Equations

- Aesop.instInhabitedForwardRulePriority.default = Aesop.ForwardRulePriority.normSafe default

Instances For

source
instance Aesop.instInhabitedForwardRulePriority :
Inhabited ForwardRulePriority
Equations

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

source
instance Aesop.instBEqForwardRulePriority :
BEq ForwardRulePriority
Equations

- Aesop.instBEqForwardRulePriority = { beq := Aesop.instBEqForwardRulePriority.beq }

source
def Aesop.instBEqForwardRulePriority.beq :
ForwardRulePriority → ForwardRulePriority → Bool
Equations

- Aesop.instBEqForwardRulePriority.beq (Aesop.ForwardRulePriority.normSafe a) (Aesop.ForwardRulePriority.normSafe b) = (a == b)
- Aesop.instBEqForwardRulePriority.beq (Aesop.ForwardRulePriority.unsafe a) (Aesop.ForwardRulePriority.unsafe b) = (a == b)
- Aesop.instBEqForwardRulePriority.beq x✝¹ x✝ = false

Instances For

source
def Aesop.ForwardRulePriority.penalty? :
ForwardRulePriority → Option Int

If a `ForwardRulePriority` contains a penalty, extract it.

Equations

- (Aesop.ForwardRulePriority.normSafe n).penalty? = some n
- (Aesop.ForwardRulePriority.unsafe p).penalty? = none

Instances For

source
def Aesop.ForwardRulePriority.successProbability? :
ForwardRulePriority → Option Percent

If a `ForwardRulePriority` contains a success probability, extract it.

Equations

- (Aesop.ForwardRulePriority.unsafe p).successProbability? = some p
- (Aesop.ForwardRulePriority.normSafe n).successProbability? = none

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.

Equations

- (Aesop.ForwardRulePriority.normSafe n).compare (Aesop.ForwardRulePriority.unsafe p) = Ordering.lt
- (Aesop.ForwardRulePriority.unsafe p).compare (Aesop.ForwardRulePriority.normSafe n) = Ordering.gt
- (Aesop.ForwardRulePriority.normSafe n₁).compare (Aesop.ForwardRulePriority.normSafe n₂) = compare n₁ n₂
- (Aesop.ForwardRulePriority.unsafe p₁).compare (Aesop.ForwardRulePriority.unsafe p₂) = (compare p₁ p₂).swap

Instances For

source
instance Aesop.ForwardRulePriority.instOrd :
Ord ForwardRulePriority
Equations

- Aesop.ForwardRulePriority.instOrd = { compare := Aesop.ForwardRulePriority.compare }

source
instance Aesop.ForwardRulePriority.instToString :
ToString ForwardRulePriority
Equations

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

source
structure Aesop.ForwardRule extends Aesop.ForwardRuleInfo :
Type

A forward rule.

- numPremises : Nat
- numLevelParams : Nat
- slotClusters : Array (Array Slot)
- conclusionDeps : Array PremiseIndex
- rulePatternInfo? : Option (RulePattern × PremiseIndex)
- name : RuleName

  The rule's name. Should be unique among all rules in a rule set.

- term : RuleTerm

  The theorem from which this rule is derived.

- prio : ForwardRulePriority

  The rule's priority.

Instances For

source
def Aesop.instInhabitedForwardRule.default :
ForwardRule
Equations

- Aesop.instInhabitedForwardRule.default = { toForwardRuleInfo := default, name := default, term := default, prio := default }

Instances For

source
instance Aesop.instInhabitedForwardRule :
Inhabited ForwardRule
Equations

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

source
instance Aesop.ForwardRule.instBEq :
BEq ForwardRule
Equations

- Aesop.ForwardRule.instBEq = { beq := fun (r₁ r₂ : Aesop.ForwardRule) => r₁.name == r₂.name }

source
instance Aesop.ForwardRule.instHashable :
Hashable ForwardRule
Equations

- Aesop.ForwardRule.instHashable = { hash := fun (r : Aesop.ForwardRule) => hash r.name }

source
instance Aesop.ForwardRule.instOrd :
Ord ForwardRule
Equations

- Aesop.ForwardRule.instOrd = { compare := fun (r₁ r₂ : Aesop.ForwardRule) => (compare r₁.prio r₂.prio).then (compare r₁.name r₂.name) }

source
instance Aesop.ForwardRule.instToString :
ToString ForwardRule
Equations

- Aesop.ForwardRule.instToString = { toString := fun (r : Aesop.ForwardRule) => toString "[" ++ toString r.prio ++ toString "] " ++ toString r.name }

source
def Aesop.ForwardRule.destruct (r : ForwardRule) :
Bool

Is this rule a `destruct` rule (i.e., should we clear matched hyps)?

Equations

- r.destruct = match r.name.builder with | Aesop.BuilderName.destruct => true | x => false

Instances For