Renaming and notations for modalities gen_proofmode
This MR implements the following renaming/new notations:
-
<subj> P
: subjectively (renamed + new notation) -
<obj> P
: objectively (renamed + new notation) -
<pers> P
: persistently (new notation) -
<affine> P
: affinely (new notation) -
<absorb> P
: absorbingly (new notation)
The following change still needs to be done, and I propose to do it in a separate MR:
-
□ P
: intuitionistically a.k.a affinely persistently
This change requires more effort and discussion. In particular, currently this modality is just a notation for the <affine> <pers> ...
, but I think it should become a Definition
:
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
(<affi> <pers> P)%I.
It being a definition reflects that fact that it will have a proper name. This will obviously break some stuff, and will require more work than just running a sed
script, hence my proposal to do that in a separate MR.
Since pretty much any commit to gen_proofmode
will break this MR, I propose to merge it ASAP.