Struct SetoidInstance 

pub struct SetoidInstance<T> {
    pub carrier: Vec<T>,
    pub equiv: fn(&T, &T) -> bool,
}

A setoid: a Rust type equipped with an explicit equivalence relation.

Mirrors the Lean 4 Setoid typeclass for use at the meta level.

Fields

carrier: Vec<T>

A representative finite sample of carrier elements.

equiv: fn(&T, &T) -> bool

The equivalence relation: equiv(a, b) iff a ~ b.

Implementations

impl<T> SetoidInstance<T>

pub fn new(carrier: Vec<T>, equiv: fn(&T, &T) -> bool) -> Self

Create a new setoid from a carrier sample and an equivalence function.

pub fn are_equiv(&self, a: &T, b: &T) -> bool

Check whether a and b are equivalent.

pub fn check_refl(&self) -> bool

Verify reflexivity for all carrier elements.

pub fn check_symm(&self) -> bool

Verify symmetry for all pairs in the carrier.

pub fn check_trans(&self) -> bool

Verify transitivity for all triples in the carrier.