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 geq based on leq
+15
src/lib.rs
+15
src/lib.rs
···
26
26
eq::Eq,
27
27
28
28
leq::Leq,
29
+
geq::Geq,
29
30
30
31
add::Add,
31
32
mul::Times,
···
61
62
// Induction
62
63
// A <= B means S(A) <= S(B)
63
64
impl<A: Nat, B: Nat> Leq<Succ<B>> for Succ<A>
65
+
where
66
+
A: Leq<B>
67
+
{}
68
+
}
69
+
70
+
pub mod geq {
71
+
use super::prelude::*;
72
+
73
+
pub trait Geq<A: Nat> {
74
+
fn geq() -> () {}
75
+
}
76
+
77
+
// If A <= B then B => A
78
+
impl<A: Nat, B: Nat> Geq<A> for B
64
79
where
65
80
A: Leq<B>
66
81
{}