Commit 094150fb authored by Robbert Krebbers's avatar Robbert Krebbers

Declare COFE on state as a canonical structure.

parent 1da4e710
......@@ -22,4 +22,6 @@ Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
( x, f x g x) icmra_map Σ f m icmra_map Σ g m.
Proof.
by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
Qed.
\ No newline at end of file
Qed.
Canonical Structure istateC Σ := leibnizC (istate Σ).
\ No newline at end of file
......@@ -2,7 +2,7 @@ Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
Record res (Σ : iParam) (A : cofeT) := Res {
wld : mapRA positive (agreeRA (laterC A));
pst : exclRA (leibnizC (istate Σ));
pst : exclRA (istateC Σ);
gst : icmra Σ (laterC A);
}.
Add Printing Constructor res.
......
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