diff --git a/tests/counter.v b/tests/counter.v index 8661b9b398eacd56c8f02234435684e6cb4848e2..8986a132626462a7db31da9255fd4a2963d53c4b 100644 --- a/tests/counter.v +++ b/tests/counter.v @@ -1,6 +1,7 @@ (* This file contains a formalization of the monotone counter, but with an explicit contruction of the monoid, as we have also done in the proof mode -paper. A version that uses the authoritative monoid and natural number monoid +paper. This should simplify explaining and understanding what is happening. +A version that uses the authoritative monoid and natural number monoid under max can be found in `heap_lang/lib/counter.v`. *) From iris.program_logic Require Export weakestpre. From iris.heap_lang Require Export lang.