Skip to content
Snippets Groups Projects
Commit f4b638e7 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Cosmetic changes in refcell.

parent adfeaec0
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/typing/unsafe/refcell/refmut_code.v
+ 1
− 3
View file @ f4b638e7
...@@ -10,8 +10,6 @@ Set Default Proof Using "Type". ...@@ -10,8 +10,6 @@ Set Default Proof Using "Type".
Section refmut_functions. Section refmut_functions.
Context `{typeG Σ, refcellG Σ}. Context `{typeG Σ, refcellG Σ}.
(* TODO : map, when we will have a nice story about closures. *)
(* Turning a refmut into a shared borrow. *) (* Turning a refmut into a shared borrow. *)
Definition refmut_deref : val := Definition refmut_deref : val :=
funrec: <> ["x"] := funrec: <> ["x"] :=
...@@ -63,7 +61,7 @@ Section refmut_functions. ...@@ -63,7 +61,7 @@ Section refmut_functions.
delete [ #1; "x"];; "return" ["r"]. delete [ #1; "x"];; "return" ["r"].
Lemma refmut_derefmut_type ty : Lemma refmut_derefmut_type ty :
typed_instruction_ty [] [] [] refmut_deref typed_instruction_ty [] [] [] refmut_derefmut
(fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
(fun '(α, β) => [# &uniq{α}(refmut β ty)]%T) (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
(fun '(α, β) => &uniq{α}ty)%T). (fun '(α, β) => &uniq{α}ty)%T).
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment