From 9f597f7b7199ec0f49f64bd860d3074cf6c287b3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 19 Jan 2016 09:57:19 +0100
Subject: [PATCH] add a (CM)RA instance for the unit type

---
 modures/cmra.v |  3 +++
 modures/ra.v   | 18 ++++++++++++++++++
 2 files changed, 21 insertions(+)

diff --git a/modures/cmra.v b/modures/cmra.v
index bce799331..b9e50b528 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -296,6 +296,9 @@ Section discrete.
 End discrete.
 Arguments discreteRA _ {_ _ _ _ _ _}.
 
+(** CMRA for the unit type *)
+Canonical Structure unitRA : cmraT := discreteRA ().
+
 (** Product *)
 Section prod.
   Context {A B : cmraT}.
diff --git a/modures/ra.v b/modures/ra.v
index a3c5d4e0b..bfc324de4 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -231,3 +231,21 @@ Ltac solve_included :=
   ra_reflection.quote;
   apply ra_reflection.flatten_correct, (bool_decide_unpack _);
   vm_compute; apply I.
+
+(** An RA for the unit type *)
+Instance unit_valid : Valid () := λ x, True.
+Instance unit_unit : Unit () := λ x, x.
+Instance unit_op : Op () := λ x y, tt.
+Instance unit_minus : Minus () := λ x y, tt.
+
+Instance unit_ra : RA ().
+Proof.
+  split; done.
+Qed.
+
+
+Instance unit_empty : Empty () := tt.
+Instance unit_empty_ra : RAIdentity().
+Proof.
+  split; done.
+Qed.
-- 
GitLab