From 2ed8bac221366425839c1d2c41e8ab8a24ec1225 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Feb 2016 18:16:13 +0100
Subject: [PATCH] CMRAIdentity instance for option.

---
 algebra/option.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/algebra/option.v b/algebra/option.v
index 367d9f0d3..4c443e3a8 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -63,6 +63,7 @@ Context {A : cmraT}.
 
 Instance option_validN : ValidN (option A) := λ n mx,
   match mx with Some x => ✓{n} x | None => True end.
+Global Instance option_empty : Empty (option A) := None.
 Instance option_unit : Unit (option A) := fmap unit.
 Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 Instance option_minus : Minus (option A) :=
@@ -125,6 +126,8 @@ Proof.
 Qed.
 Canonical Structure optionRA :=
   CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.
+Global Instance option_cmra_identity : CMRAIdentity optionRA.
+Proof. split. done. by intros []. by inversion_clear 1. Qed.
 
 Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
 Proof.
-- 
GitLab