From 8be90cca01b2c58bcde904f35e2d1fcdd7342beb Mon Sep 17 00:00:00 2001 From: colin Date: Wed, 20 Jul 2022 02:48:59 -0700 Subject: [PATCH] coremem_types: add `Next` type to Peano numbers --- crates/types/src/compound/peano.rs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/crates/types/src/compound/peano.rs b/crates/types/src/compound/peano.rs index 83a199e..d3825e4 100644 --- a/crates/types/src/compound/peano.rs +++ b/crates/types/src/compound/peano.rs @@ -2,14 +2,20 @@ pub struct PNext

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

{} +impl Peano for P0 { + type Next = P1; +} +impl Peano for PNext

{ + type Next = PNext>; +} impl PeanoNonZero for PNext

{ type Prev = P; }