gnat 0.1.9

Type-level numbers without extra bounds
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

use super::*;

// AddIf(C, L, R) := if C { L + R } else { R }
//                 = L + if C { R } else { 0 }
type _AddIf<C, L, R> = If<C, add::_Add<L, R>, L>;

// Double(N) := 2 * N
type _Double<N> = PushBit<N, crate::lit!(0)>;

// Mul(L, R) := L * R
//
// H := H(L), P := P(L)
//
// L * R = (2 * H + P) * R
//       = 2 * (H * R) + P * R
//       = 2 * (H * R) + if P { R } else { 0 }
//       = AddIf(P, Double(H * R), R)
#[apply(nat_expr)]
pub type _Mul<L: NatExpr, R: NatExpr> = If<
    L,
    _AddIf<
        _P<L>, //
        _Double<_Mul<_H<L>, R>>,
        R,
    >,
    // 0 * R = 0
    crate::lit!(0),
>;

/// Type-level [`*`](core::ops::Mul)
#[doc(alias = "*")]
#[apply(opaque)]
#[apply(test_op! test_mul, L * R)]
pub type Mul<L, R> = _Mul;