diff --git a/stdpp/gmap.v b/stdpp/gmap.v index 8f28f260ae2072322102b963034912ad0e5734fc..309f308936e2abac063e35971a760c82dc6f6bd3 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