Naming bikeshed: Persistently and affinely-persistently
gen_proofmode, the name "persistently" and the typeclass "Persistent" do not match the notation
I think this is a great name for "the context that behaves like normal intuitionistic logic", so I think ideally we should call
□ "persistently" here as well, and define
Persistent P := P |- □ P. This requires finding a new name for the modality that is in the BI interface -- the modality that allows duplication, but does not allow throwing things away. IIRC @jtassaro called this modality "relevant". That doesn't seem like the worst possible name, though "relevantly" sounds a little funny?
To be clear, I suggest keeping the name "persistent" for the
□ and the "persistent context". If we change that name, it would affect affine Iris, and I don't think we want to rename this symbol there again.