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

use std::marker::PhantomData;

pub trait SealedNat {}

pub trait Nat: SealedNat + Send + Copy + 'static
{
  #[allow(non_upper_case_globals)]
  const Value: Self;

  fn nat() -> Self;
}

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

#[derive(Copy, Clone)]
pub struct S<N>(pub PhantomData<N>);

impl SealedNat for Z {}

impl Nat for Z
{
  #[allow(non_upper_case_globals)]
  const Value: Z = Z;

  fn nat() -> Z
  {
    Z
  }
}

impl<N> SealedNat for S<N> where N: Nat {}

impl<N> Nat for S<N>
where
  N: Nat,
{
  #[allow(non_upper_case_globals)]
  const Value: S<N> = S(PhantomData);

  fn nat() -> S<N>
  {
    S(PhantomData)
  }
}

pub fn succ<N>(_: N) -> S<N>
{
  S(PhantomData)
}