From ff244cf1b7deabfd9bc1e4eae0bc48db6aedbe77 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 20 May 2018 17:00:53 +0200
Subject: [PATCH] also show Box conversions

---
 theories/typing/lib/cell.v | 36 +++++++++++++++++++++++++++++-------
 1 file changed, 29 insertions(+), 7 deletions(-)

diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 4c5145d0..4afcfed7 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -115,22 +115,44 @@ Section typing.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_jump; [solve_typing..|]. rewrite /tctx_incl /=.
-    iIntros (??) "_ _ $". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
-    by iIntros "$".
+    iApply type_jump; [solve_typing..|].
+    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   Definition cell_from_mut : val :=
     funrec: <> ["x"] := return: ["x"].
 
   Lemma cell_from_mut_type ty `{!TyWf ty} :
-    typed_val cell_get_mut (fn(∀ α, ∅; &uniq{α} ty) → &uniq{α} (cell ty)).
+    typed_val cell_from_mut (fn(∀ α, ∅; &uniq{α} ty) → &uniq{α} (cell ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_jump; [solve_typing..|].
+    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+  Qed.
+
+  Definition cell_into_box : val :=
+    funrec: <> ["x"] := return: ["x"].
+
+  Lemma cell_into_box_type ty `{!TyWf ty} :
+    typed_val cell_into_box (fn(∅;box (cell ty)) → box ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_jump; [solve_typing..|]. rewrite /tctx_incl /=.
-    iIntros (??) "_ _ $". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
-    by iIntros "$".
+    iApply type_jump; [solve_typing..|].
+    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+  Qed.
+
+  Definition cell_from_box : val :=
+    funrec: <> ["x"] := return: ["x"].
+
+  Lemma cell_from_box_type ty `{!TyWf ty} :
+    typed_val cell_from_box (fn(∅; box ty) → box (cell ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_jump; [solve_typing..|].
+    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   (** Reading from a cell *)
-- 
GitLab