ecsolticia.codeberg.page
Compile-time construction of Peano axioms-based natural numbers and addition, multiplication, and exponentiation defined through them within Rust. (Mirrored from Codeberg)
rename operations
+21
-23
+18
-18
src/lib.rs
+18
-18
src/lib.rs
···
29
geq::Geq,
30
31
add::Add,
32
-
mul::Times,
33
exp::Exp,
34
35
parity::Even,
···
85
use super::prelude::*;
86
87
pub trait Add<RHS: Nat> {
88
-
type Result: Nat;
89
}
90
91
// Base case
92
// N + 0 = N
93
impl<T: Nat> Add<_0> for T {
94
-
type Result = T;
95
}
96
97
// Induction
···
100
where
101
A: Add<B>
102
{
103
-
type Result = Succ<<A as Add<B>>::Result>;
104
}
105
}
106
107
pub mod mul {
108
use super::prelude::*;
109
110
-
pub trait Times<RHS: Nat> {
111
-
type Result: Nat;
112
}
113
114
// Base case
115
// N * 0 = 0
116
-
impl<T: Nat> Times<_0> for T {
117
-
type Result = _0;
118
}
119
120
// Induction
121
// A * S(B) = A * B + A
122
-
impl<A: Nat, B: Nat> Times<Succ<B>> for A
123
where
124
-
A: Times<B>,
125
-
<A as Times<B>>::Result: Add<A>
126
{
127
-
type Result = <<A as Times<B>>::Result as Add<A>>::Result;
128
}
129
}
130
131
pub mod exp {
132
use super::prelude::*;
133
134
-
pub trait Exp<Pow: Nat> {
135
-
type Result: Nat;
136
}
137
138
// Base case
139
// N ^ 0 = 1
140
impl<T: Nat> Exp<_0> for T {
141
-
type Result = _1;
142
}
143
144
// Induction
···
146
impl<A: Nat, B: Nat> Exp<Succ<B>> for A
147
where
148
A: Exp<B>,
149
-
<A as Exp<B>>::Result: Times<A>
150
{
151
-
type Result =
152
-
<<A as Exp<B>>::Result as Times<A>>::Result;
153
}
154
}
155
···
29
geq::Geq,
30
31
add::Add,
32
+
mul::Mul,
33
exp::Exp,
34
35
parity::Even,
···
85
use super::prelude::*;
86
87
pub trait Add<RHS: Nat> {
88
+
type Sum: Nat;
89
}
90
91
// Base case
92
// N + 0 = N
93
impl<T: Nat> Add<_0> for T {
94
+
type Sum = T;
95
}
96
97
// Induction
···
100
where
101
A: Add<B>
102
{
103
+
type Sum = Succ<<A as Add<B>>::Sum>;
104
}
105
}
106
107
pub mod mul {
108
use super::prelude::*;
109
110
+
pub trait Mul<RHS: Nat> {
111
+
type Prod: Nat;
112
}
113
114
// Base case
115
// N * 0 = 0
116
+
impl<T: Nat> Mul<_0> for T {
117
+
type Prod = _0;
118
}
119
120
// Induction
121
// A * S(B) = A * B + A
122
+
impl<A: Nat, B: Nat> Mul<Succ<B>> for A
123
where
124
+
A: Mul<B>,
125
+
<A as Mul<B>>::Prod: Add<A>
126
{
127
+
type Prod = <<A as Mul<B>>::Prod as Add<A>>::Sum;
128
}
129
}
130
131
pub mod exp {
132
use super::prelude::*;
133
134
+
pub trait Exp<P: Nat> {
135
+
type Pow: Nat;
136
}
137
138
// Base case
139
// N ^ 0 = 1
140
impl<T: Nat> Exp<_0> for T {
141
+
type Pow = _1;
142
}
143
144
// Induction
···
146
impl<A: Nat, B: Nat> Exp<Succ<B>> for A
147
where
148
A: Exp<B>,
149
+
<A as Exp<B>>::Pow: Mul<A>
150
{
151
+
type Pow =
152
+
<<A as Exp<B>>::Pow as Mul<A>>::Prod;
153
}
154
}
155
+3
-5
src/main.rs
+3
-5
src/main.rs
···
1
-
#![recursion_limit = "132"]
2
-
3
use rspeano::prelude::*;
4
5
fn five_plus_five_is_ten() {
6
-
type Claimed10 = <_5 as Add<_5>>::Result;
7
8
type Verified10 =
9
Succ< // 1
···
23
}
24
25
fn four_times_two_is_eight() {
26
-
type Claimed8 = <_4 as Times<_2>>::Result;
27
28
type Verified8 =
29
Succ< // 1
···
41
}
42
43
fn two_squared_is_four() {
44
-
type Claimed4 = <_2 as Exp<_2>>::Result;
45
46
type Verified4 =
47
Succ<
···
1
use rspeano::prelude::*;
2
3
fn five_plus_five_is_ten() {
4
+
type Claimed10 = <_5 as Add<_5>>::Sum;
5
6
type Verified10 =
7
Succ< // 1
···
21
}
22
23
fn four_times_two_is_eight() {
24
+
type Claimed8 = <_4 as Mul<_2>>::Prod;
25
26
type Verified8 =
27
Succ< // 1
···
39
}
40
41
fn two_squared_is_four() {
42
+
type Claimed4 = <_2 as Exp<_2>>::Pow;
43
44
type Verified4 =
45
Succ<