Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
FP
Stacked Borrows Coq
Commits
3476c8a5
Commit
3476c8a5
authored
Jul 05, 2019
by
Hai Dang
Browse files
WIP: mapsto
parent
f8968978
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/sim/cmra.v
View file @
3476c8a5
...
...
@@ -34,6 +34,9 @@ Definition to_heapletR (h: mem) : heapletR := fmap to_agree h.
Definition
to_ptrmapUR
(
pm
:
ptrmap
)
:
ptrmapUR
:=
fmap
(
λ
tm
,
(
to_tagKindR
tm
.1
,
to_heapletR
tm
.2
))
pm
.
Definition
lmap
:=
gmap
loc
(
scalar
*
stack
).
Definition
lmapUR
:=
gmapR
loc
(
csumR
(
exclR
(
leibnizO
(
scalar
*
stack
)))
(
agreeR
unitO
)).
Definition
res
:=
(
ptrmap
*
cmap
)
%
type
.
Definition
resUR
:=
prodUR
ptrmapUR
cmapUR
.
Definition
to_resUR
(
r
:
res
)
:
resUR
:=
(
to_ptrmapUR
r
.1
,
to_cmapUR
r
.2
).
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment