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.

instance Aesop.instInhabitedForwardRulePriority : Inhabited ForwardRulePriority

instance Aesop.instBEqForwardRulePriority : BEq ForwardRulePriority

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

If a ForwardRulePriority contains a penalty, extract it.

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

If a ForwardRulePriority contains a success probability, extract it.

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.

instance Aesop.ForwardRulePriority.instOrd : Ord ForwardRulePriority

instance Aesop.ForwardRulePriority.instToString : ToString ForwardRulePriority

structure Aesop.ForwardRuleextends 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.

instance Aesop.instInhabitedForwardRule : Inhabited ForwardRule

instance Aesop.ForwardRule.instBEq : BEq ForwardRule

instance Aesop.ForwardRule.instHashable : Hashable ForwardRule

instance Aesop.ForwardRule.instOrd : Ord ForwardRule

instance Aesop.ForwardRule.instToString : ToString ForwardRule

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

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