From 80e1b1d7ea8fd2d933549e4dea65ac62942b7c4d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Sep 2020 11:19:50 +0200
Subject: [PATCH] add some missing functors
---
theories/algebra/gmap.v | 3 +++
theories/algebra/list.v | 5 ++++-
2 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 6e3b7311a..025d04df0 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -680,3 +680,6 @@ Instance gmapRF_contractive K `{Countable K} F :
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
Qed.
+
+Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor :=
+ urFunctor_to_rFunctor $ gmapURF K F.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 50ceac0f1..d1f9f0c3b 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -186,7 +186,7 @@ Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
Qed.
-(* CMRA *)
+(* CMRA. Only works if [A] has a unit! *)
Section cmra.
Context {A : ucmraT}.
Implicit Types l : list A.
@@ -571,3 +571,6 @@ Instance listURF_contractive F :
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
Qed.
+
+Definition listRF (F : urFunctor) : rFunctor :=
+ urFunctor_to_rFunctor $ listURF F.
--
GitLab