Commit 8af24118 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix.

parent 2a11f567
Pipeline #16767 passed with stage
in 16 minutes and 36 seconds
......@@ -6,6 +6,7 @@
Q : iProp Σ
l : loc
v : val
IPM_INTERNAL : IPM_STATE 3
============================
"Hl" : l ↦ v
--------------------------------------∗
......@@ -36,6 +37,7 @@
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
......@@ -68,6 +70,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
......@@ -99,6 +102,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅
......@@ -131,6 +135,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
......@@ -196,6 +201,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 1
============================
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy
......
......@@ -5,6 +5,7 @@
hd, acc : val
xs, ys : list val
Φ : val → iPropI Σ
IPM_INTERNAL : IPM_STATE 2
============================
"Hxs" : is_list hd xs
"Hys" : is_list acc ys
......@@ -16,6 +17,7 @@
Σ : gFunctors
heapG0 : heapG Σ
IPM_INTERNAL : IPM_STATE 2
acc : val
ys : list val
Φ : val → iPropI Σ
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment