Update changelog

agda · Aug 30, 2024 · beba170 · beba170
1 parent 98881dd
commit beba170
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -44,6 +44,11 @@ Non-backwards compatible changes
  As a result many of the `Composition` lemmas now take a proof of
  transitivity and the `Identity` lemmas now take a proof of reflexivity.
 
+* 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.
+
 * The module `IO.Primitive` was moved to `IO.Primitive.Core`.
 
 Minor improvements