From 8862cf75693430ecdfdbea9ddeae0c897e11579d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 15 Oct 2020 12:18:52 +0200
Subject: [PATCH] add gmap_view type notation (mirroring auth)
---
theories/algebra/lib/gmap_view.v | 15 +++++++++++----
1 file changed, 11 insertions(+), 4 deletions(-)
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index abe12c6cf..d94c5caa4 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -94,12 +94,19 @@ End rel.
Local Existing Instance gmap_view_rel_discrete.
-Definition gmap_viewUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
- viewUR (gmap_view_rel K V).
-Definition gmap_viewR (K : Type) `{Countable K} (V : ofeT) : cmraT :=
- viewR (gmap_view_rel K V).
+(** [gmap_view] is a notation to give canonical structure search the chance
+to infer the right instances (see [auth]). *)
+Notation gmap_view K V := (view (@gmap_view_rel_raw K _ _ V)).
Definition gmap_viewO (K : Type) `{Countable K} (V : ofeT) : ofeT :=
viewO (gmap_view_rel K V).
+Definition gmap_viewR (K : Type) `{Countable K} (V : ofeT) : cmraT :=
+ viewR (gmap_view_rel K V).
+Definition gmap_viewUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
+ viewUR (gmap_view_rel K V).
+
+(** Make sure the notation does not mix up its arguments. *)
+Local Definition gmap_view_check {K : Type} `{Countable K} {V : ofeT} :
+ gmap_view K V = gmap_viewO K V := eq_refl.
Section definitions.
Context {K : Type} `{Countable K} {V : ofeT}.
--
GitLab