Multiple rules write S is persistent, but the notion of a proposition being persistent is not defined.
In Iris proper we have:
P is persistent
------------------
P |- \persistently P
This could also be used to mark the persistent propositions True, t =_\tau t'and{P} e {Q}`, which currently have separate
rules.
Multiple rules write
S is persistent, but the notion of a proposition being persistent is not defined.In Iris proper we have:
This could also be used to mark the persistent propositions
True, t =_\tau t'and{P} e {Q}`, which currently have separaterules.