# Figure out the best place for the plainly modality

Right now, `plainly`

is part of the BI interface, so *every* logic has to have this modality. Given that this modality is not at all needed for the proof mode to function, I think that's a bad choice. We already have some rather arbitrary-looking axioms for `bi_persistently`

; let's try to minimize the amount of "strange modalities" in the interface(s) as much as possible.

The following proposals are on the table:

- Follow !98 (closed) and treat
`plainly`

like`fupd`

and`bupd`

: As "standardized extensions" that come with their own separate interface, but once instantiated with proofs of the basic laws are automatically integrated into the proofmode (because a bunch of instances based on this interface already exist). - Put
`plainly`

into`Sbi`

. - Have a new "IrisLikeLogic", extending
`Sbi`

, which contains`plainly`

as well as the update modalities.

My own comments:

- This is the most general and, absent technical concerns, "best" solution -- but handling the resulting hierarchie(s) could become annoying. We'd also have to decide which approach to use for these (bundled/unbundled, typeclasses/canonical structures). (I somehow thought @robbertkrebbers was able to solve all hierarchy problems in Coq as that's what you did so far; hearing even you say that this is getting too complicated is quite unsettling to be honest ;)
- I see no motivation for doing this, it seems rather arbitrary.
- seems okay to me -- a little sad, but given the state of affairs probably a reasonable compromise for the time being. We have no example of a logic that would benefit from
`plainly`

that doesn't also have the updates.

Ideally I'd prefer 1., but given that if @robbertkrebbers can't get the hierarchy to work, neither will I -- that makes 3. look appealing enough. ;) I don't like 2. at all.