Skip to content
Snippets Groups Projects
Commit c4f2d1ee authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

WIP.

parent 23b0aee0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 4 additions and 6 deletions
theories/typing/sum.v
+ 4
− 6
View file @ c4f2d1ee
...@@ -183,12 +183,10 @@ Section sum. ...@@ -183,12 +183,10 @@ Section sum.
Lemma emp_sum E L : Lemma emp_sum E L :
eqtype E L emp (sum []). eqtype E L emp (sum []).
Proof. Proof.
split; (iIntros (q) "_ _"; iSplit; first done; iSplit; iAlways). apply eqtype_unfold. iIntros (?) "_ !# _".
- iIntros (??) "[]". iSplit; first done; iSplit; iAlways; iIntros; iSplit; try by iIntros "[]".
- iIntros (κ tid l) "[]". - iIntros "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)". by rewrite nth_empty.
- iIntros (??) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)". - iIntros "H". iDestruct "H" as (i) "(_ & Hshr)". by rewrite nth_empty.
by rewrite nth_empty.
- iIntros (???) "H". iDestruct "H" as (i) "(_ & Hshr)". by rewrite nth_empty.
Qed. Qed.
Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl). Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl).
......
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