From 0db3bed9ab658d57500543cf464dc4023175e5c1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 16 Dec 2016 12:07:42 +0100
Subject: [PATCH] comment on the need for a lifetime token in sharing

---
 theories/typing/type.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index ddb31f4f..4a538b7f 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -30,11 +30,15 @@ Section type.
          namespace N, for allowing more flexibility for the user of
          this type (typically for the [own] type). AFAIK, there is no
          fundamental reason for this.
-
          This should not be harmful, since sharing typically creates
          invariants, which does not need the mask.  Moreover, it is
          more consistent with thread-local tokens, which we do not
-         give any. *)
+         give any.
+ 
+         The lifetime token is needed (a) to make the definition of simple types
+         nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
+         we can have emp == sum [].
+       *)
       ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
         lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗
         ty_shr κ tid (↑N) l ∗ q.[κ];
-- 
GitLab