Skip to content
Snippets Groups Projects

Fix proof after iris!1035.

Merged Fix proof after iris!1035.
snyke7/lambda-rust:ike/fix_limit_iframe_ex into master
Merged Ike Mulder requested to merge snyke7/lambda-rust:ike/fix_limit_iframe_ex into master
Compare
and
1 file
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
theories/typing/own.v
+ 1
− 1
@@ -234,7 +234,7 @@ Section typing.
iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iExists l, _, _. iSplitR; first done.
iFrame "∗#"; auto.
iFrame "∗#". by iIntros "!> $".
Qed.
Lemma read_own_move E L ty n :