Struct EqualityWitness 

pub struct EqualityWitness<T> {
    pub value: T,
}

A witness that two Rust values are equal.

Constructed only when the equality holds, providing a type-indexed proof analogous to Lean 4’s Eq.refl.

Fields

value: T

The value for which equality was witnessed.

Implementations

impl<T: PartialEq + Clone> EqualityWitness<T>

pub fn try_new(a: &T, b: &T) -> Option<Self>

Attempt to construct an EqualityWitness for a == b.

Returns Some only when a == b.

pub fn cast<'a>(&self, a: &'a T) -> &'a T

Use the witness to cast one reference to another.

Because the witness guarantees equality, we can use a as b.

Trait Implementations

impl<T: Clone> Clone for EqualityWitness<T>

fn clone(&self) -> EqualityWitness<T>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T: Debug> Debug for EqualityWitness<T>

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

Formats the value using the given formatter.

impl<T: PartialEq> PartialEq for EqualityWitness<T>

fn eq(&self, other: &EqualityWitness<T>) -> 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<T: Eq> Eq for EqualityWitness<T>

impl<T> StructuralPartialEq for EqualityWitness<T>