Commit 34dcb910 authored by Ralf Jung's avatar Ralf Jung

construct the resource functor

parent dbf38eb5
......@@ -6,6 +6,7 @@ COFEs to the category of CMRAs, which is instantiated with [laterC iProp]. The
[laterC iProp] can be used to construct impredicate CMRAs, such as the stored
propositions using the agreement CMRA. *)
(* TODO RJ: Can we make use of resF, the resource functor? *)
Module iProp.
Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
uPredC (resRA Λ Σ (laterC A)).
......
......@@ -215,3 +215,14 @@ Proof.
* by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
* by apply optionC_map_ne, ifunctor_map_ne.
Qed.
Program Definition resF {Λ Σ} : iFunctor := {|
ifunctor_car := resRA Λ Σ;
ifunctor_map A B := resC_map
|}.
Next Obligation.
intros Λ Σ A x. by rewrite /= res_map_id.
Qed.
Next Obligation.
intros Λ Σ A B C f g x. by rewrite /= res_map_compose.
Qed.
Markdown is supported
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