Skip to content
Snippets Groups Projects
Commit 85c15c64 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

More clean up

parent ba3fae4a
No related branches found
No related tags found
No related merge requests found
Pipeline #27754 passed
Hide whitespace changes
Inline Side-by-side
theories/examples/subprotocols.v
+ 2
− 2
View file @ 85c15c64
...@@ -6,7 +6,7 @@ Section basics. ...@@ -6,7 +6,7 @@ Section basics.
Lemma reference_example (l2' : loc) : Lemma reference_example (l2' : loc) :
l2' ↦ #22 -∗ l2' ↦ #22 -∗
(<! (l1 l2 : loc)> MSG (#l1, #l2) {{ l1 ↦ #20 ∗ l2 ↦ #22 }}; END)%proto ⊑ (<! (l1 l2 : loc)> MSG (#l1, #l2) {{ l1 ↦ #20 ∗ l2 ↦ #22 }}; END)%proto ⊑
(<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END)%proto. (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END)%proto.
Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame. Qed. Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed.
End pair. End pair.
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