Tactics issues
I was trying to use iInv
to open an Iris invariant around an iProp WP. iInv
fails, I think, because it cannot solve atomic
.
Somehow the instance base_atomic_atomic
was not used. I was able to use it manually though (see https://gitlab.mpi-sws.org/FP/gpfsl/blob/sc_inv/theories/sc_invariants.v).
Another one is that wp_write
currently doesn't support l ↦ ?
, which I doubt that it's due to Coq not being able to match against ?
. Should we change the notation then?