ferrite_session/internal/functional/
nat.rs

1use std::marker::PhantomData;
2
3pub trait SealedNat {}
4
5pub trait Nat: SealedNat + Send + Copy + 'static
6{
7  #[allow(non_upper_case_globals)]
8  const Value: Self;
9
10  fn nat() -> Self;
11}
12
13#[derive(Copy, Clone)]
14pub struct Z;
15
16#[derive(Copy, Clone)]
17pub struct S<N>(pub PhantomData<N>);
18
19impl SealedNat for Z {}
20
21impl Nat for Z
22{
23  #[allow(non_upper_case_globals)]
24  const Value: Z = Z;
25
26  fn nat() -> Z
27  {
28    Z
29  }
30}
31
32impl<N> SealedNat for S<N> where N: Nat {}
33
34impl<N> Nat for S<N>
35where
36  N: Nat,
37{
38  #[allow(non_upper_case_globals)]
39  const Value: S<N> = S(PhantomData);
40
41  fn nat() -> S<N>
42  {
43    S(PhantomData)
44  }
45}
46
47pub fn succ<N>(_: N) -> S<N>
48{
49  S(PhantomData)
50}