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)
impl leq
+27
src/lib.rs
+27
src/lib.rs
···
20
20
Nat,
21
21
Succ,
22
22
_0,
23
+
23
24
eq::Eq,
24
25
eq::ProofEq,
26
+
27
+
leq::Leq,
28
+
leq::ProofLeq,
29
+
25
30
add::Add,
26
31
mul::Times,
27
32
exp::Exp
···
40
45
41
46
// Define equality of naturals
42
47
impl<T: Nat> Eq<T, T> for ProofEq<T, T> {}
48
+
}
49
+
50
+
pub mod leq {
51
+
use super::prelude::*;
52
+
53
+
pub trait Leq<A: Nat, B: Nat> {
54
+
fn check() -> () {}
55
+
}
56
+
57
+
pub struct ProofLeq<A: Nat, B: Nat>(A, B);
58
+
59
+
// Base case
60
+
// 0 <= N for every N
61
+
impl<A: Nat> Leq<_0, A> for ProofLeq<_0, A> {}
62
+
63
+
// Induction
64
+
// A <= B means S(A) <= S(B)
65
+
impl<A: Nat, B: Nat> Leq<Succ<A>, Succ<B>> for
66
+
ProofLeq<Succ<A>, Succ<B>>
67
+
where
68
+
ProofLeq<A, B>: Leq<A, B>
69
+
{}
43
70
}
44
71
45
72
pub mod add {