Modular Concurrent Counter Module: The RA of the ILN does not match the one in Coq #7
Description
The Modular Concurrent Counter presented in Section 13.1 used the RA Auth((Q_{01} × N)_?), as opposed to `(Q_{01} × Ag Z), which is used in Coq (https://gitlab.mpi-sws.org/iris/examples/-/blob/master/theories/lecture_notes/modular_incr.v).
This may be because Agree is not widely used (or even presented?) in the ILN.