add/clean up some TODOs for copying

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} :

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. *)