1#![no_std]
2
3use core::ops::*;
4
5#[derive(Copy)] pub enum Zero {}
6#[derive(Clone, Copy)] pub struct Succ<N: Natural>(N);
7
8impl Clone for Zero {
9 fn clone(&self) -> Self { match *self {} }
10}
11
12pub trait Natural {
13 fn to_usize() -> usize;
14}
15
16impl Natural for Zero {
17 fn to_usize() -> usize { 0 }
18}
19
20impl<N: Natural> Natural for Succ<N> {
21 fn to_usize() -> usize { 1+N::to_usize() }
22}
23
24impl<N: Natural> Add<N> for Zero {
25 type Output = N;
26 fn add(self: Zero, n: N) -> N { n }
27}
28
29impl<M: Natural, N: Natural> Add<N> for Succ<M> where M: Add<N>, <M as Add<N>>::Output: Natural {
30 type Output = Succ<<M as Add<N>>::Output>;
31 fn add(self: Succ<M>, n: N) -> Self::Output { let Succ(m) = self; Succ(m+n) }
32}