Enum CcStep 

pub enum CcStep {
    Hyp(usize),
    Refl(usize),
    Sym(usize),
    Trans(usize, usize),
    Cong(usize, usize),
}

One step of an equality proof.

Five rules, and between them they are the whole of equational logic on a first-order term language. A congruence-closure ENGINE is a fixpoint over an e-graph with a union-find and use lists; a PROOF that one particular equation is in that closure is this list, and checking it needs neither. That asymmetry is the entire reason a second kernel can afford to look at try_cc at all.

Variants

Hyp(usize)

The goal’s i-th equality hypothesis, as it stands.

Refl(usize)

t = t, for the term at table index t.

Sym(usize)

From step i proving a = b, conclude b = a.

Trans(usize, usize)

From step i proving a = b and step j proving b = c, conclude a = c.

Cong(usize, usize)

From step i proving f = g and step j proving x = y, conclude f x = g y.

Trait Implementations

impl Clone for CcStep

fn clone(&self) -> CcStep

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CcStep

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

Formats the value using the given formatter.

impl PartialEq for CcStep

fn eq(&self, other: &CcStep) -> 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 Eq for CcStep

impl StructuralPartialEq for CcStep