ty_ops/
nat.rs

1use std::marker::PhantomData;
2use crate::*;
3use crate::classes::*;
4
5
6#[derive(Copy, Clone, Default)]
7pub struct Z;
8
9#[derive(Copy, Clone, Default)]
10pub struct S<T> (PhantomData<T>);
11
12#[derive(Copy, Clone, Default)]
13pub struct Nat;
14
15impl Type for Nat {}
16
17impl Eq for Nat {}
18
19impl Value for Z {
20    type Type = Nat;
21}
22
23impl<T: Value<Type=Nat>> Value for S<T> {
24    type Type = Nat;
25}
26
27// eq
28
29impl App<Z> for EqTo<Z> {
30    type Result = True;
31}
32
33impl<T: Value<Type=Nat>> App<Z> for EqTo<S<T>> {
34    type Result = False;
35}
36
37impl<T: Value<Type=Nat>> App<S<T>> for EqTo<Z> {
38    type Result = False;
39}
40
41impl<L: Value<Type=Nat>, R: Value<Type=Nat>, Eq: Value<Type=Bool>> App<S<R>> for EqTo<S<L>>
42    where EqTo<L>: App<R, Result=Eq>
43{
44    type Result = Eq;
45}
46
47
48// Add
49pub type Add<A, B> = Eval<AddOn<A>, B>;
50#[derive(Copy, Clone, Default)]
51pub struct AddOn<A: Value<Type=Nat>>(PhantomData<A>);
52
53impl<A: Value<Type=Nat>> Value for AddOn<A> {
54    type Type = Lambda<Nat, Nat>;
55}
56
57impl<A: Value<Type=Nat>> App<Z> for AddOn<A> {
58    type Result = A;
59}
60
61impl<A: Value<Type=Nat>, B: Value<Type=Nat>, R: Value<Type=Nat>> App<S<B>> for AddOn<A>
62    where
63        AddOn<A>: Value<Type=Lambda<Nat, Nat>> + App<B, Result=R>
64{
65    type Result = S<R>;
66}
ty_ops/nat.rs

ty_ops/
nat.rs
