From e491cf4719393995de7d0c5500ad2fe51beeba1b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Oct 2020 13:33:38 +0200
Subject: [PATCH] add some FIXME so we do not forget to make the gmap_view API
 consistent with the rest

---
 theories/algebra/lib/gmap_view.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 7cc89e990..5439678fe 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -243,6 +243,8 @@ Section lemmas.
     rewrite -cmra_valid_validN singleton_op singleton_valid.
     by rewrite -pair_op pair_valid to_agree_op_valid.
   Qed.
+  (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
+     have [inv_L] lemmas instead that just have an equality on the RHS. *)
   Lemma gmap_view_frag_op_valid_L `{!LeibnizEquiv V} k dq1 dq2 v1 v2 :
     ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 = v2.
   Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
@@ -277,6 +279,8 @@ Section lemmas.
     ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
     ✓ dq ∧ m !! k ≡ Some v.
   Proof. rewrite gmap_view_both_frac_valid. naive_solver done. Qed.
+  (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
+     have [inv_L] lemmas instead that just have an equality on the RHS. *)
   Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
     ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
     ✓ dq ∧ m !! k = Some v.
-- 
GitLab