From 00b874ce429f0ece220c24c995a8b27a8cc67470 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 9 Apr 2018 09:58:23 +0200
Subject: [PATCH] ofe_funC_ofe_discrete and ofe_funR_cmra_discrete.

---
 theories/algebra/functions.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index 6983a95f3..e3c368d1a 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -17,6 +17,10 @@ Section ofe.
   Implicit Types x : A.
   Implicit Types f g : ofe_fun B.
 
+  Global Instance ofe_funC_ofe_discrete :
+    (∀ i, OfeDiscrete (B i)) → OfeDiscrete (ofe_funC B).
+  Proof. intros HB f f' Heq i. apply HB, Heq. Qed.
+
   (** Properties of ofe_fun_insert. *)
   Global Instance ofe_fun_insert_ne x :
     NonExpansive2 (ofe_fun_insert (B:=B) x).
@@ -52,6 +56,10 @@ Section cmra.
   Implicit Types x : A.
   Implicit Types f g : ofe_fun B.
 
+  Global Instance ofe_funR_cmra_discrete:
+    (∀ i, CmraDiscrete (B i)) → CmraDiscrete (ofe_funR B).
+  Proof. intros HB. split; [apply _|]. intros x Hv i. apply HB, Hv. Qed.
+
   Global Instance ofe_fun_singleton_ne x :
     NonExpansive (ofe_fun_singleton x : B x → _).
   Proof. intros n y1 y2 ?; apply ofe_fun_insert_ne. done. by apply equiv_dist. Qed.
-- 
GitLab