diff --git a/CHANGELOG.md b/CHANGELOG.md index f64ab9dea17745aa54dc4aee4ccbe4c2db1cba45..502634f90a19ef0418f9b1ff4f767ec21eea18b8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,12 @@ lemma. [discardable fraction](iris/algebra/dfrac.v) (`dfrac`) instead of a fraction (`frac`). Lemmas affected by this have been renamed such that the "frac" in their name has been changed into "dfrac". (by Simon Friis Vindum) +* Equip `mono_nat` algebra with support for `dfrac`, make API more consistent, + and add notation for algebra elements. See `iris/algebra/lib/mono_nat.v` for + details. This affects some existing terms and lemmas: + - `mono_nat_auth` now takes a `dfrac`, but the recommendation is to port to the notation. + - `mono_nat_auth_frac_op`, `mono_nat_lb_op`: direction of equality is swapped. + - `mono_nat_auth_frac_valid`, `mono_nat_both_frac_valid`: use `dfrac` variant instead. **Changes in `bi`:**