Struct PropEq 

pub struct PropEq {
    pub ty: Expr,
    pub lhs: Expr,
    pub rhs: Expr,
}

Propositional equality record, carrying the type and both sides.

Used to represent equality propositions a = b : α as data structures during elaboration and pretty-printing.

Fields

ty: Expr

The common type of both sides.

lhs: Expr

The left-hand side.

rhs: Expr

The right-hand side.

Implementations

impl PropEq

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

Construct a new propositional equality.

pub fn refl(ty: Expr, a: Expr) -> Self

Construct the reflexivity equality a = a.

pub fn is_refl(&self) -> bool

Returns true if this is a reflexivity equality (lhs == rhs).

pub fn symm(self) -> Self

Swap sides: a = b becomes b = a.

pub fn trans(self, other: Self) -> Option<Self>

Chain two equalities: a = b and b = c become a = c.

Returns None if the rhs of self differs from the lhs of other.

pub fn display(&self) -> String

Display as a human-readable string.

Trait Implementations

impl Clone for PropEq

fn clone(&self) -> PropEq

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PropEq

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

Formats the value using the given formatter.

impl PartialEq for PropEq

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

impl StructuralPartialEq for PropEq