diff --git a/crates/types/src/compound/mod.rs b/crates/types/src/compound/mod.rs index d17e233..56578a2 100644 --- a/crates/types/src/compound/mod.rs +++ b/crates/types/src/compound/mod.rs @@ -1 +1,2 @@ pub mod list; +pub mod peano; diff --git a/crates/types/src/compound/peano.rs b/crates/types/src/compound/peano.rs new file mode 100644 index 0000000..83a199e --- /dev/null +++ b/crates/types/src/compound/peano.rs @@ -0,0 +1,15 @@ +pub struct PNext

(P); +pub struct P0; +pub type P1 = PNext; + +pub trait Peano { } + +pub trait PeanoNonZero { + type Prev: Peano; +} + +impl Peano for P0 { } +impl Peano for PNext

{} +impl PeanoNonZero for PNext

{ + type Prev = P; +}