coremem_types: add Next type to Peano numbers

This commit is contained in:
2022-07-20 02:48:59 -07:00
parent 5ad6af8f8b
commit 8be90cca01

View File

@@ -2,14 +2,20 @@ pub struct PNext<P>(P);
pub struct P0; pub struct P0;
pub type P1 = PNext<P0>; pub type P1 = PNext<P0>;
pub trait Peano { } pub trait Peano {
type Next: PeanoNonZero;
}
pub trait PeanoNonZero { pub trait PeanoNonZero {
type Prev: Peano; type Prev: Peano;
} }
impl Peano for P0 { } impl Peano for P0 {
impl<P: Peano> Peano for PNext<P> {} type Next = P1;
}
impl<P: Peano> Peano for PNext<P> {
type Next = PNext<PNext<P>>;
}
impl<P: Peano> PeanoNonZero for PNext<P> { impl<P: Peano> PeanoNonZero for PNext<P> {
type Prev = P; type Prev = P;
} }