make _0 the unit type · ecsolticia.codeberg.page/rspeano@36574ce

Compile-time construction of Peano axioms-based natural numbers and addition, multiplication, and exponentiation defined through them within Rust. (Mirrored from Codeberg)

fork atom

make _0 the unit type

ecsolticia.codeberg.page 6 months ago 36574ce3 2df9b890

+1 -1

1 changed file

expand all

unified split

src

lib.rs

+1 -1

src/lib.rs

··· 2 2 pub struct Succ<T>(T); 3 3 4 4 // Inductively define naturals 5 - pub type _0 = Succ<()>; 5 + pub type _0 = (); 6 6 impl Nat for _0 {} 7 7 impl<T: Nat> Nat for Succ<T> {} 8 8