comment

cmcmA20 · Oct 11, 2024 · d35dde9 · d35dde9
1 parent 7c50e7e
commit d35dde9
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Order/Constructions/Nat.agda b/src/Order/Constructions/Nat.agda
@@ -33,6 +33,7 @@ Suc : ℕₚ ⇒ ℕₚ
 Suc .hom    = suc
 Suc .pres-≤ = s≤s
 
+-- NB avoid using it in computational code
 compare-nat : (m n : ℕ) → (m ≤ n) ⊎ (m ≥ n)
 compare-nat 0       _ = inl z≤
 compare-nat (suc m) 0 = inr z≤