From 054ac622947272d9d095bca2e2fb116c92defa7e Mon Sep 17 00:00:00 2001
From: Sanjit Bhat <sanjit.bhat@gmail.com>
Date: Fri, 19 Jul 2024 09:26:40 -0400
Subject: [PATCH] docs(gmap): add galina escaping

---
 stdpp/gmap.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/stdpp/gmap.v b/stdpp/gmap.v
index 8f28f260..309f3089 100644
--- a/stdpp/gmap.v
+++ b/stdpp/gmap.v
@@ -15,9 +15,8 @@ has the same good properties:
 
 Compared to [Pmap], we not only need to make sure the trie representation is
 canonical, we also need to make sure that all positions (of type positive) are
-valid encodings of [K]. That is, for each position [q] in the trie, we have:
-
-  encode <$> decode q = Some q
+valid encodings of [K]. That is, for each position [q] in the trie, we have
+[encode <$> decode q = Some q].
 
 Instead of formalizing this condition using a Sigma type (which would break
 the strict positivity check in nested recursive definitions), we make
-- 
GitLab