Commit 06571377 authored by Ralf Jung's avatar Ralf Jung
Browse files

tests/counter.v: explain purpose

parent c3731066
(* This file contains a formalization of the monotone counter, but with an (* 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 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`. *) under max can be found in `heap_lang/lib/counter.v`. *)
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment