Commit d8a82b35 authored by Ralf Jung's avatar Ralf Jung

show that we can construct an IParam from a single, constant cmra (not using the functor)

parent c9ae33d4
Require Export modures.cmra iris.language.
Set Bullet Behavior "Strict Subproofs".
Record iParam := IParam {
iexpr : Type;
ival : Type;
istate : Type;
icmra : cofeT cmraT;
ilanguage : Language iexpr ival istate;
icmra : cofeT cmraT;
icmra_empty A : Empty (icmra A);
icmra_empty_spec A : RAIdentity (icmra A);
icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
......@@ -15,6 +17,7 @@ Record iParam := IParam {
icmra_map (g f) x icmra_map g (icmra_map f x);
icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
}.
Arguments IParam _ _ _ _ _ {_ _} _ {_ _ _ _}.
Existing Instances ilanguage.
Existing Instances icmra_empty icmra_empty_spec icmra_map_ne icmra_map_mono.
......@@ -24,4 +27,16 @@ Proof.
by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
Qed.
Canonical Structure istateC Σ := leibnizC (istate Σ).
\ No newline at end of file
Definition IParamConst (iexpr ival istate : Type)
(ilanguage : Language iexpr ival istate)
(icmra : cmraT) {icmra_empty : Empty icmra}
{icmra_empty_spec : RAIdentity icmra}:
iParam.
eapply (IParam iexpr ival istate ilanguage
(fun _ => icmra) (fun _ _ _ => cid)).
Unshelve.
- by intros.
- by intros.
Defined.
Canonical Structure istateC Σ := leibnizC (istate Σ).
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