From ed4332632775eb6d5ce50f4baa6de534c385e726 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 17 Jan 2022 10:42:43 -0500
Subject: [PATCH] changelog
---
CHANGELOG.md | 3 +++
1 file changed, 3 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index dc605ae0e..9e14f5f3e 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`:**
--
GitLab