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

Starting the work on arc.

parent d5d2f89a
No related branches found
No related tags found
No related merge requests found
Pipeline #
......@@ -55,6 +55,7 @@ theories/typing/lib/cell.v
theories/typing/lib/spawn.v
theories/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v
theories/typing/lib/arc.v
theories/typing/lib/mutex/mutex.v
theories/typing/lib/mutex/mutexguard.v
theories/typing/lib/refcell/refcell.v
......
This diff is collapsed.
This diff is collapsed.
......@@ -8,6 +8,8 @@ From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
Set Default Proof Using "Type".
(* TODO : weak_count strong_count *)
Definition rc_stR :=
prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitC))) natUR.
Class rcG Σ :=
......
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