number_types/
add.rs

1use crate::*;
2
3pub trait Add<Rhs: Number>: Number {
4    type Output: Number;
5}
6
7impl<Rhs: Number> Add<Rhs> for Zero {
8    type Output = Rhs;
9}
10
11// basic positive addition
12/* (0 + 1) + (0 + 1):
13Successor<Zero> as
14    Add<
15        N = Zero as Add<N = Zero, Rhs = Successor<Zero>, Output = Successor<Zero>>,
16        Rhs = Successor<Zero>,
17        Output = Successor<T::O>
18    >
19*/
20impl<N: Number, Rhs: Number, O: Number> Add<Rhs> for Successor<N>
21where
22    Rhs: IsPositive,
23    N: Add<Rhs, Output = O>,
24{
25    type Output = Successor<O>;
26}
27
28// -a + b = -(a - b)
29impl<N: Number, Rhs: Number, O: Number> Add<Rhs> for Negative<N>
30where
31    Rhs: IsPositive,
32    N: Sub<Rhs, Output = O>,
33    O: Neg,
34{
35    type Output = <O as Neg>::Output;
36}
37
38// a + -b = a - b
39impl<N: Number, Rhs: Number, O: Number> Add<Negative<Rhs>> for Successor<N>
40where
41    Successor<N>: Sub<Rhs, Output = O>,
42{
43    type Output = O;
44}
45// -a + -b = -(a + b)
46impl<N: Number, Rhs: Number> Add<Negative<Rhs>> for Negative<N>
47where
48    N: Add<Rhs>,
49{
50    type Output = Negative<<N as Add<Rhs>>::Output>;
51}
52
53pub trait AddOp {
54    type Output: Number;
55}
56
57impl<Lhs, Rhs: Number> AddOp for Op<Lhs, Rhs>
58where
59    Lhs: Add<Rhs>,
60{
61    type Output = <Lhs as Add<Rhs>>::Output;
62}
number_types/add.rs

number_types/
add.rs
