Skip to content
Snippets Groups Projects
Verified Commit 054ac622 authored by Sanjit Bhat's avatar Sanjit Bhat
Browse files

docs(gmap): add galina escaping

parent 9e2c5234
No related branches found
No related tags found
1 merge request!557docs(gmap): add galina escaping
...@@ -15,9 +15,8 @@ has the same good properties: ...@@ -15,9 +15,8 @@ has the same good properties:
Compared to [Pmap], we not only need to make sure the trie representation is 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 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: valid encodings of [K]. That is, for each position [q] in the trie, we have
[encode <$> decode q = Some q].
encode <$> decode q = Some q
Instead of formalizing this condition using a Sigma type (which would break Instead of formalizing this condition using a Sigma type (which would break
the strict positivity check in nested recursive definitions), we make the strict positivity check in nested recursive definitions), we make
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment