Struct SimpRule 

pub struct SimpRule {
    pub name: String,
    pub binders: Vec<(String, Term)>,
    pub lhs: Term,
    pub rhs: Term,
    pub head: String,
}

The @[simp] registry’s compiled rule — Context::simp_rules/simp_rules_for hand these to whatever does the rewriting, already destructured into ∀x̄. lhs ⟶ rhs. A @[simp] lemma COMPILED to the form a rewriter applies: ∀x̄. lhs ⟶ rhs.

The binders are the lemma’s universally quantified variables in order; lhs and rhs mention them as Term::Var. head is lhs’s head symbol and is the registry’s dispatch key — see Context::simp_rules_for.

Fields

name: String

The lemma’s name, so a rewrite can say which lemma fired.

binders: Vec<(String, Term)>

Universally quantified variables, outermost first, with their types.

lhs: Term

The pattern to match.

rhs: Term

What to replace a match with.

head: String

lhs’s head symbol — the dispatch key.

Implementations

impl SimpRule

pub fn compile(name: &str, stmt: &Term) -> KernelResult<SimpRule>

Compile a declared statement Π(x̄). Eq A lhs rhs into a rule, or say why it is not one.

pub fn rewrite(&self, term: &Term) -> Option<Term>

Try to rewrite term with this rule AT THE TOP LEVEL — first-order matching of lhs against term, then rhs under the resulting substitution. None means the rule does not apply; the caller descends into subterms itself.

This lives with the rule rather than with the rewriter for one reason: matching has to agree with what SimpRule::compile refused. A rewriter that wrote its own matcher could bind a pattern variable twice to two different terms, or substitute a variable the rule never bound — and both are silent wrong answers rather than failures.

pub fn matching(&self, term: &Term) -> Option<Vec<Term>>

The instance of the rule’s variables, in binder order, that makes lhs read as term at the top level; None when the rule does not match there or leaves a variable undetermined.

Trait Implementations

impl Clone for SimpRule

fn clone(&self) -> SimpRule

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SimpRule

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for SimpRule

fn eq(&self, other: &SimpRule) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for SimpRule