Skip to content
Snippets Groups Projects
Commit 22cd25ab authored by Ralf Jung's avatar Ralf Jung
Browse files

Cell::get_mut does not need the type to be copy

parent 089b2cd3
No related branches found
No related tags found
No related merge requests found
......@@ -103,7 +103,7 @@ Section typing.
Definition cell_get_mut : val :=
funrec: <> ["x"] := "return" ["x"].
Lemma cell_get_mut_type `(!Copy ty) :
Lemma cell_get_mut_type ty :
typed_instruction_ty [] [] [] cell_get_mut
(fn (λ α, [α])%EL (λ α, [# &uniq{α} (cell ty)])%T (λ α, &uniq{α} ty)%T).
Proof.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment