computation-types 0.0.0

Types for abstract mathematical computation
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64

pub use self::{add::*, max::*};

#[derive(Clone, Copy, Debug)]
pub struct Zero;

#[derive(Clone, Copy, Debug)]
pub struct Suc<A>(A);

pub type One = Suc<Zero>;
pub type Two = Suc<One>;

mod max {
    use super::*;

    pub trait Max<B> {
        type Max;
    }

    impl Max<Zero> for Zero {
        type Max = Zero;
    }

    impl<A> Max<Zero> for Suc<A> {
        type Max = Suc<A>;
    }

    impl<B> Max<Suc<B>> for Zero {
        type Max = Suc<B>;
    }

    impl<A, B> Max<Suc<B>> for Suc<A>
    where
        A: Max<B>,
    {
        type Max = Suc<<A as Max<B>>::Max>;
    }
}

mod add {
    use super::*;

    pub trait Add<B> {
        type Add;
    }

    impl Add<Zero> for Zero {
        type Add = Zero;
    }

    impl<A> Add<Zero> for Suc<A> {
        type Add = Suc<A>;
    }

    impl<B> Add<Suc<B>> for Zero {
        type Add = Suc<B>;
    }

    impl<A, B> Add<Suc<B>> for Suc<A>
    where
        A: Add<B>,
    {
        type Add = Suc<Suc<<A as Add<B>>::Add>>;
    }
}