diff --git a/CHANGELOG.md b/CHANGELOG.md index dc605ae0eef83407c954bf9064a7f22df1f169c9..9e14f5f3e11afe059baa8afa2a96746ae7819d8b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,6 +31,9 @@ lemma. - `mono_nat_auth_frac_op`, `mono_nat_auth_frac_op_valid`, `mono_nat_auth_frac_valid`, `mono_nat_both_frac_valid`: use `dfrac` variant instead. +* Add `mono_list` algebra for monotonically growing lists with an exclusive + authoritative element and persistent prefix witnesses. See + `iris/algebra/lib/mono_list.v` for details. **Changes in `bi`:**