Struct CongrHypothesis 

pub struct CongrHypothesis {
    pub lhs: Expr,
    pub rhs: Expr,
    pub is_heq: bool,
}

A hypothesis in a congruence lemma.

Records the type of an equality hypothesis that must be provided.

Fields

lhs: Expr

Left-hand side of the equality.

rhs: Expr

Right-hand side of the equality.

is_heq: bool

Whether this is a heterogeneous equality.

Implementations

impl CongrHypothesis

pub fn eq(lhs: Expr, rhs: Expr) -> Self

Create a homogeneous equality hypothesis lhs = rhs.

pub fn heq(lhs: Expr, rhs: Expr) -> Self

Create a heterogeneous equality hypothesis HEq lhs rhs.

pub fn is_trivial(&self) -> bool

Check if this is a trivial hypothesis (lhs = lhs).

Trait Implementations

impl Clone for CongrHypothesis

fn clone(&self) -> CongrHypothesis

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CongrHypothesis

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

Formats the value using the given formatter.