From d8a82b35bb8175fa03fd38eabf238d3af3e4564f Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 19 Jan 2016 09:16:03 +0100
Subject: [PATCH] show that we can construct an IParam from a single, constant
 cmra (not using the functor)

---
 iris/parameter.v | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/iris/parameter.v b/iris/parameter.v
index 671bdbab7..7bb6d313e 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -1,11 +1,13 @@
 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 Σ).
-- 
GitLab