Struct EqChain 

pub struct EqChain {
    pub ty: Expr,
    pub steps: Vec<PropEq>,
}

A chain of propositional equalities a₀ = a₁ = … = aₙ.

Useful for representing calc-block-style equality chains during elaboration.

Fields

ty: Expr

The type of all elements.

steps: Vec<PropEq>

The sequence of steps; steps[i].rhs == steps[i+1].lhs.

Implementations

impl EqChain

pub fn new(ty: Expr) -> Self

Create an empty chain for a given type.

pub fn push(&mut self, step: PropEq)

Extend the chain with a new equality step.

Panics if the step’s lhs does not match the last rhs.

pub fn collapse(self) -> Option<PropEq>

Collapse the chain to a single equality (if non-empty).

pub fn is_empty(&self) -> bool

Returns true if the chain is empty.

pub fn len(&self) -> usize

Number of steps in the chain.

Trait Implementations

impl Clone for EqChain

fn clone(&self) -> EqChain

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EqChain

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

Formats the value using the given formatter.