From 876c6af5385aa166b6ed76beee3b26c88db2b037 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 20 Feb 2022 10:30:44 -0500
Subject: [PATCH] explain why we prove Cell: Copy

---
 theories/typing/lib/cell.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 7d200730..f4325de4 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -49,6 +49,10 @@ Section cell.
   Lemma cell_proper' E L ty1 ty2 : eqtype E L ty1 ty2 → eqtype E L (cell ty1) (cell ty2).
   Proof. eapply cell_proper. Qed.
 
+  (* The real [Cell] in Rust is never [Copy], but that is mostly for reasons of
+     ergonomics -- it is widely agreed that it would be sound for [Cell] to be
+     [Copy]. [Cell] is also rather unique as an interior mutable [Copy] type, so
+     proving this is a good benchmark. *)
   Global Instance cell_copy ty :
     Copy ty → Copy (cell ty).
   Proof.
-- 
GitLab