Skip to content
Snippets Groups Projects
Commit 96edbfda authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'fix-meta-token-doc' into 'master'

Fix argument order in comment.

See merge request iris/iris!506
parents e014ddc3 7d0b39f2
No related branches found
No related tags found
No related merge requests found
...@@ -17,7 +17,7 @@ of a location [l], this mechanism allows one to attach "meta" or "ghost" data to ...@@ -17,7 +17,7 @@ of a location [l], this mechanism allows one to attach "meta" or "ghost" data to
locations. This is done as follows: locations. This is done as follows:
- When one allocates a location, in addition to the point-to connective [l ↦ v], - When one allocates a location, in addition to the point-to connective [l ↦ v],
one also obtains the token [meta_token ⊤ l]. This token is an exclusive one also obtains the token [meta_token l ⊤]. This token is an exclusive
resource that denotes that no meta data has been associated with the resource that denotes that no meta data has been associated with the
namespaces in the mask [⊤] for the location [l]. namespaces in the mask [⊤] for the location [l].
- Meta data tokens can be split w.r.t. namespace masks, i.e. - Meta data tokens can be split w.r.t. namespace masks, i.e.
......
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