Trait Setoid 

pub trait Setoid {
    // Required method
    fn equiv(&self, other: &Self) -> bool;

    // Provided methods
    fn refl(&self) -> bool { ... }
    fn symm(&self, other: &Self) -> bool { ... }
}

A setoid: a type equipped with an equivalence relation.

This is the Rust-level analogue of Lean 4’s Setoid typeclass, used for quotiented types and proof-irrelevant equality.

Required Methods

fn equiv(&self, other: &Self) -> bool

The equivalence relation.

Provided Methods

fn refl(&self) -> bool

Reflexivity of the equivalence.

fn symm(&self, other: &Self) -> bool

Symmetry: if self ~ other then other ~ self.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<T: PartialEq> Setoid for T