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.
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.