Struct CheckedEquiv 

pub struct CheckedEquiv { /* private fields */ }

A checked equivalence with its witness proof.

Implementations

impl CheckedEquiv

pub fn refl(id: u64) -> Self

Creates a reflexive equivalence.

pub fn by_axiom(lhs: u64, rhs: u64, name: impl Into<String>) -> Self

Creates a named-axiom equivalence.

pub fn lhs(&self) -> u64

Returns the LHS hash.

pub fn rhs(&self) -> u64

Returns the RHS hash.

pub fn proof(&self) -> &EquivProofTerm

Returns a reference to the proof term.

pub fn is_trivial(&self) -> bool

Returns true if both sides are identical.