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)
refactor eq and leq to use single generic parameters
+18
-20
+11
-17
src/lib.rs
+11
-17
src/lib.rs
···
15
15
pub type _6 = Succ<_5>;
16
16
pub type _7 = Succ<_6>;
17
17
pub type _8 = Succ<_7>;
18
+
pub type _9 = Succ<_8>;
19
+
pub type _10 = Succ<_9>;
18
20
19
21
pub use super::{
20
22
Nat,
···
22
24
_0,
23
25
24
26
eq::Eq,
25
-
eq::ProofEq,
26
27
27
28
leq::Leq,
28
-
leq::ProofLeq,
29
29
30
30
add::Add,
31
31
mul::Times,
···
39
39
pub mod eq {
40
40
use super::prelude::*;
41
41
42
-
pub trait Eq<A: Nat, B: Nat> {
43
-
fn check() -> () {}
42
+
pub trait Eq<A: Nat> {
43
+
fn equal() -> () {}
44
44
}
45
-
46
-
pub struct ProofEq<A: Nat, B: Nat>(A, B);
47
-
impl<A: Nat, B: Nat> ProofEq<A, B> {}
48
45
49
46
// Define equality of naturals
50
-
impl<T: Nat> Eq<T, T> for ProofEq<T, T> {}
47
+
impl<A: Nat> Eq<A> for A {}
51
48
}
52
49
53
50
pub mod leq {
54
51
use super::prelude::*;
55
52
56
-
pub trait Leq<A: Nat, B: Nat> {
57
-
fn check() -> () {}
53
+
pub trait Leq<A: Nat> {
54
+
fn leq() -> () {}
58
55
}
59
56
60
-
pub struct ProofLeq<A: Nat, B: Nat>(A, B);
61
-
62
57
// Base case
63
58
// 0 <= N for every N
64
-
impl<A: Nat> Leq<_0, A> for ProofLeq<_0, A> {}
65
-
59
+
impl<A: Nat> Leq<A> for _0 {}
60
+
66
61
// Induction
67
62
// A <= B means S(A) <= S(B)
68
-
impl<A: Nat, B: Nat> Leq<Succ<A>, Succ<B>> for
69
-
ProofLeq<Succ<A>, Succ<B>>
63
+
impl<A: Nat, B: Nat> Leq<Succ<B>> for Succ<A>
70
64
where
71
-
ProofLeq<A, B>: Leq<A, B>
65
+
A: Leq<B>
72
66
{}
73
67
}
74
68
+7
-3
src/main.rs
+7
-3
src/main.rs
···
17
17
_0
18
18
>>>>>>>>>>;
19
19
20
-
ProofEq::<Claimed10, Verified10>::check();
20
+
<Claimed10 as Eq<Verified10>>::equal();
21
21
}
22
22
23
23
fn four_times_two_is_eight() {
···
35
35
_0
36
36
>>>>>>>>;
37
37
38
-
ProofEq::<Claimed8, Verified8>::check();
38
+
<Claimed8 as Eq<Verified8>>::equal();
39
39
}
40
40
41
41
fn two_squared_is_four() {
···
49
49
_0
50
50
>>>>;
51
51
52
-
ProofEq::<Claimed4, Verified4>::check();
52
+
<Claimed4 as Eq<Verified4>>::equal();
53
53
}
54
54
55
55
fn main() {
···
68
68
69
69
// fails:
70
70
// _5::even();
71
+
72
+
<_3 as Leq<_4>>::leq();
73
+
// fails:
74
+
// <_3 as Leq<_2>>::leq();
71
75
}