Struct SimpSet 

pub struct SimpSet { /* private fields */ }

An indexed set of simp rules.

Implementations

impl SimpSet

pub fn new() -> Self

pub fn len(&self) -> usize

pub fn is_empty(&self) -> bool

pub fn register_lemma(&mut self, name: &str, lemma: &ProofExpr) -> bool

Compile and index lemma as a rewrite rule. Returns false (and registers nothing) if the lemma is not an oriented rule: no equational or iff core, a bare-variable lhs, rhs/condition variables the lhs does not bind, or shadowed binder names.

The rule’s derivation base is a PremiseMatch leaf, so the lemma must be in scope (a premise or hypothesis) wherever the rule fires.

Trait Implementations

impl Default for SimpSet

fn default() -> SimpSet

Returns the “default value” for a type.