Update changelog

agda · Sep 2, 2024 · 165fd71 · 165fd71
1 parent 68769e2
commit 165fd71
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -15,6 +15,11 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The implementation of `≤-total` in `Data.Nat.Properties` has been altered
+  to use operations backed by primitives, rather than recursion, making it
+  significantly faster. However, its reduction behaviour on open terms may have
+  changed.
+
 Minor improvements
 ------------------