Skip to content
Snippets Groups Projects
Commit 95e76f9d authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' into 'master'

docs(gmap): add galina escaping

Closes #211

See merge request iris/stdpp!557
parents 9e2c5234 054ac622
No related branches found
No related tags found
1 merge request!557docs(gmap): add galina escaping
Pipeline #104224 passed
...@@ -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