From fe271b0adaf0a030b0a419f317c933c088870dd9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dani=C3=ABl=20Louwrink?= <daniel.louwrink@gmail.com>
Date: Fri, 24 Apr 2020 14:33:17 +0200
Subject: [PATCH] add/clean up some TODOs for copying

---
 theories/logrel/copying.v | 7 ++++++-
 theories/logrel/types.v   | 4 ++--
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/theories/logrel/copying.v b/theories/logrel/copying.v
index 56e1968..acc0030 100644
--- a/theories/logrel/copying.v
+++ b/theories/logrel/copying.v
@@ -23,6 +23,11 @@ Section copying.
     ⊢ copy A <: A.
   Proof. by iIntros (v) "!> #H". Qed.
 
+  (* TODO(COPY): have A <: copy- A rule *)
+  (* TODO(COPY): Show derived rules about copyability of products, sums, etc. *)
+  (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
+
+  (* TODO(COPY) *)
   Lemma coreP_desired_lemma (P : iProp Σ) :
     □ (P -∗ □ P) -∗ coreP P -∗ P.
   Proof.
@@ -102,7 +107,7 @@ Section copying.
         iExists A; repeat iModIntro; iApply "Hv".
   Qed.
 
-  (* TODO: Do the forall type former, once we have the value restriction *)
+  (* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
 
   (* Copyability of recursive types *)
   Lemma lty_rec_copy C `{!Contractive C} :
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 7380b53..5925e56 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -472,7 +472,7 @@ Section properties.
     by iModIntro.
   Qed.
 
-  (* FIXME: copy *)
+  (* TODO(COPY) *)
   (* Lemma ltyped_load_copy A {copyA : LTyCopy A} : *)
   (*   ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut A. *)
   (* Proof. *)
@@ -526,7 +526,7 @@ Section properties.
     by iExists m.
   Qed.
 
-  (* FIXME: copy *)
+  (* TODO(COPY) *)
   (* Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} : *)
   (*   ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A). *)
   (* Proof. *)
-- 
GitLab