Make notation for pure and plainly affine
I think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use *
and -*
even when working in linear Iris.
I think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use *
and -*
even when working in linear Iris.