From 06571377c04ea59c744fd6dc2fc71a40c11d2f24 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Mon, 31 Oct 2016 14:12:35 +0100
Subject: [PATCH] tests/counter.v: explain purpose
---
tests/counter.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/tests/counter.v b/tests/counter.v
index 8661b9b3..8986a132 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.
--
2.26.2