Enum CongrProof 

pub enum CongrProof {
    Refl(Expr),
    Symm(Box<CongrProof>),
    Trans(Box<CongrProof>, Box<CongrProof>),
    Congr(Box<CongrProof>, Box<CongrProof>),
    Hyp(Name),
}

A proof of an equality in the congruence closure.

Variants

Refl(Expr)

refl a: a = a.

Symm(Box<CongrProof>)

symm p: p proves a = b, so symm proves b = a.

Trans(Box<CongrProof>, Box<CongrProof>)

trans p q: p proves a = b and q proves b = c.

Congr(Box<CongrProof>, Box<CongrProof>)

congr p q: p proves f = g and q proves a = b, so (f a) = (g b).

Hyp(Name)

hyp name: an equality hypothesis.

Implementations

impl CongrProof

pub fn depth(&self) -> usize

Compute the depth of the proof term.

pub fn is_refl(&self) -> bool

Check if the proof is a trivial reflexivity.

pub fn hypothesis_count(&self) -> usize

Count the number of hypothesis uses.

pub fn simplify(self) -> Self

Simplify double negations (symm (symm p) → p).

Trait Implementations

impl Clone for CongrProof

fn clone(&self) -> CongrProof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CongrProof

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

Formats the value using the given formatter.