- Add modes missing from stdpp's base.v, except for sets (and maps).
- Add most missing modes from ofe.v and cmra.v
I expect landing this to not be trivial, so let me encourage cherry-picking and work-stealing from the outset.
UPDATED: The example for
Equiv lives at https://gitlab.mpi-sws.org/Blaisorblade/iris/-/commits/modes-broken, on top of this MR. It seems to work but in the end we agreed to not include it.
In fact, Iris builds here with the
Equiv mode with few fixes, despite the bug @robbertkrebbers identified, so I added the extra commits.