From 5de3c7f7aae92b0493100a21741904c1194bb91a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 May 2021 19:05:34 +0200
Subject: [PATCH] Parentheses.
---
theories/fin_maps.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e04532a1..34bf85b6 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2562,10 +2562,10 @@ Section kmap.
rewrite lookup_kmap_is_Some. naive_solver.
Qed.
Lemma lookup_kmap {A} (m : M1 A) (i : K1) :
- kmap f m !! f i = m !! i.
+ kmap f m !! (f i) = m !! i.
Proof. apply option_eq. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
Lemma lookup_total_kmap `{Inhabited A} (m : M1 A) (i : K1) :
- kmap f m !!! f i = m !!! i.
+ kmap f m !!! (f i) = m !!! i.
Proof. by rewrite !lookup_total_alt, lookup_kmap. Qed.
Global Instance kmap_inj {A} : Inj (=@{M1 A}) (=) (kmap f).
--
GitLab