From beba170a5bfd3106903358d00cb329bdae92a996 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 30 Aug 2024 16:17:01 +0200 Subject: [PATCH] Update changelog --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index bb6e91c887..1be5e109d4 100644 --- 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