From 380e265116936177deeeb65a20efb3955b4da837 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 May 2020 13:14:00 +0200
Subject: [PATCH] Comment about `BiLaterMixin`.

---
 theories/bi/interface.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 7b153697c..5a460db1c 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -114,6 +114,17 @@ Section bi_mixin.
     bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
   }.
 
+  (** We equip any BI with a later modality. This avoids an additional layer in
+  the BI hierachy and improves performance significantly (see Iris issue #303).
+
+  For non step-indexed BIs the later modality can simply be defined as the
+  identity function, as the Löb axiom or contractiveness of later is not part of
+  [BiLaterMixin]. For step-indexed BIs one should separately prove an instance
+  of the class [BiLöb PROP] or [Contractive (▷)]. (Note that there is an
+  instance [Contractive (▷) → BiLöb PROP] in [derived_laws_sbi].)
+
+  For non step-indexed BIs one can get a "free" instance of [BiLaterMixin] using
+  the smart constructor [bi_later_mixin_id] below. *)
   Context (bi_later : PROP → PROP).
   Local Notation "â–· P" := (bi_later P) : bi_scope.
 
-- 
GitLab