fin-part-ord 0.1.0

Datatype for finite partial orders
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

/// Laws:
///
/// - Reflexivity: `self.le(x, x) == true`
/// - Antisymmetry: `self.le(x, y) && self.le(y, x) ==> x == y`
/// - Transitivity: `self.le(x, y) && self.le(y, z) ==> self.le(x, z)`
/// - Compatibility: `self.le(x, y) <==> x == y || self.lt(x, y)`
/// - Add/less: `{ self.add(x, y); self.le(x, y) } == true`
pub trait FinPartOrd<T>
where
    Self: Sized,
{
    type Error;

    #[must_use]
    fn empty() -> Self;

    fn add(self, lo: T, hi: T) -> Result<Self, Self::Error>;

    /// Check if one element is less than another.
    ///
    /// May return `true` when `lo == hi`, even if that element hasn't been
    /// explicitly added.
    fn lt(&self, lo: &T, hi: &T) -> Result<bool, Self::Error>;

    /// May return `true` when `lo == hi`, even if that element hasn't been
    /// explicitly added.
    fn le(&self, lo: &T, hi: &T) -> Result<bool, Self::Error>
    where
        T: PartialEq,
    {
        if lo == hi {
            return Ok(true);
        }
        self.lt(lo, hi)
    }
}