Struct SimpLemmaSet 

pub struct SimpLemmaSet { /* private fields */ }

A collection of simp lemmas that can be applied in sequence.

Implementations

impl SimpLemmaSet

pub fn new() -> Self

Create an empty lemma set.

pub fn add(&mut self, lemma: SimpLemma)

Add a lemma.

pub fn len(&self) -> usize

Number of lemmas.

pub fn is_empty(&self) -> bool

Check if empty.

pub fn apply_once(&self, expr: &Expr) -> (Expr, bool)

Apply all lemmas in order to an expression (one pass).

pub fn apply_all(&self, expr: &Expr) -> Expr

Apply all lemmas exhaustively (until no changes).

pub fn iter(&self) -> impl Iterator<Item = &SimpLemma>

Iter over lemmas.

pub fn find(&self, name: &Name) -> Option<&SimpLemma>

Look up a lemma by name.

Trait Implementations

impl Default for SimpLemmaSet

fn default() -> Self

Returns the “default value” for a type.