computation_types/
peano.rs

1pub use self::{add::*, max::*};
2
3#[derive(Clone, Copy, Debug)]
4pub struct Zero;
5
6#[derive(Clone, Copy, Debug)]
7pub struct Suc<A>(A);
8
9pub type One = Suc<Zero>;
10pub type Two = Suc<One>;
11
12mod max {
13    use super::*;
14
15    pub trait Max<B> {
16        type Max;
17    }
18
19    impl Max<Zero> for Zero {
20        type Max = Zero;
21    }
22
23    impl<A> Max<Zero> for Suc<A> {
24        type Max = Suc<A>;
25    }
26
27    impl<B> Max<Suc<B>> for Zero {
28        type Max = Suc<B>;
29    }
30
31    impl<A, B> Max<Suc<B>> for Suc<A>
32    where
33        A: Max<B>,
34    {
35        type Max = Suc<<A as Max<B>>::Max>;
36    }
37}
38
39mod add {
40    use super::*;
41
42    pub trait Add<B> {
43        type Add;
44    }
45
46    impl Add<Zero> for Zero {
47        type Add = Zero;
48    }
49
50    impl<A> Add<Zero> for Suc<A> {
51        type Add = Suc<A>;
52    }
53
54    impl<B> Add<Suc<B>> for Zero {
55        type Add = Suc<B>;
56    }
57
58    impl<A, B> Add<Suc<B>> for Suc<A>
59    where
60        A: Add<B>,
61    {
62        type Add = Suc<Suc<<A as Add<B>>::Add>>;
63    }
64}
computation_types/peano.rs

computation_types/
peano.rs
