Enum EquivProofTerm 

pub enum EquivProofTerm {
    Refl(u64),
    Symm(Box<EquivProofTerm>),
    Trans(Box<EquivProofTerm>, Box<EquivProofTerm>),
    Axiom(String),
}

A proof term witnessing an equivalence.

Variants

Refl(u64)

Reflexivity: a ≡ a.

Symm(Box<EquivProofTerm>)

Symmetry: if a ≡ b then b ≡ a.

Trans(Box<EquivProofTerm>, Box<EquivProofTerm>)

Transitivity: if a ≡ b and b ≡ c then a ≡ c.

Axiom(String)

A named axiom.

Implementations

impl EquivProofTerm

pub fn depth(&self) -> usize

Returns the depth of the proof term.

pub fn is_refl(&self) -> bool

Returns true if the proof is trivially reflexive.

Trait Implementations

impl Clone for EquivProofTerm

fn clone(&self) -> EquivProofTerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EquivProofTerm

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

Formats the value using the given formatter.