Commit 84278e1b authored by Robbert Krebbers's avatar Robbert Krebbers

Agree is a functor.

parent 91c5bb27
...@@ -124,7 +124,7 @@ Proof. ...@@ -124,7 +124,7 @@ Proof.
Qed. Qed.
End agree. End agree.
Canonical Structure agreeC (A : cmraT) : cmraT := CMRAT (agree A). Canonical Structure agreeRA (A : cofeT) : cmraT := CMRAT (agree A).
Section agree_map. Section agree_map.
Context `{Cofe A, Cofe B} (f: A B) `{Hf: n, Proper (dist n ==> dist n) f}. Context `{Cofe A, Cofe B} (f: A B) `{Hf: n, Proper (dist n ==> dist n) f}.
...@@ -147,3 +147,6 @@ Section agree_map. ...@@ -147,3 +147,6 @@ Section agree_map.
try apply Hxy; eauto using agree_valid_le. try apply Hxy; eauto using agree_valid_le.
Qed. Qed.
End agree_map. End agree_map.
Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B :=
CofeMor (agree_map f : agreeRA A agreeRA B).
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