From ca02a39cff99d0c996b7cc69602afff0d6fc569a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 Jul 2023 17:25:56 +0000
Subject: [PATCH] Improve comment.
---
iris/bi/interface.v | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 13df9945d..cce7437ae 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -94,10 +94,13 @@ Section bi_mixin.
bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
}.
- (** We equip any BI with a persistence modality that carves out the
- intuitionistically fragment of the separation logic. For logics such as Iris,
+ (** We require any BI to have a persistence modality that carves out the
+ intuitionistic fragment of the separation logic. For logics such as Iris,
the persistence modality has a non-trivial definition (involving the [core] of
- the camera). However, for some simpler discrete BIs the persistence modality
+ the camera). It is not clear whether a trivial definition exists: while
+ [<pers> P := False] comes close, it does not satisfy [later_persistently_1].
+
+ However, for some simpler discrete BIs the persistence modality
can be defined as:
<pers> P := ⌜ emp ⊢ P âŒ
--
GitLab