Commit 5d384541 authored by Ralf Jung's avatar Ralf Jung

explain why we expose κ' in bor_acc_strong

parent aa650418
Pipeline #31162 passed with stage
in 33 minutes and 36 seconds
......@@ -27,7 +27,7 @@ Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
(* Deriving this just to prove that it can be derived.
(It is in the signature only for code sharing reasons.*)
(It is in the signature only for code sharing reasons.) *)
Lemma bor_shorten_ κ κ' P : κ κ' - &{κ'}P - &{κ}P.
iIntros "#Hκκ'". rewrite !bor_unfold_idx. iDestruct 1 as (i) "[#? ?]".
......@@ -126,6 +126,8 @@ Module Type lifetime_sig.
lft_ctx - &{κ,i}P - idx_bor_own q i ={E,E∖↑lftN}=
( P ( P ={E∖↑lftN,E}= idx_bor_own q i))
([†κ] |={E∖↑lftN,E}=> idx_bor_own q i).
(* We have to expose κ' here as without [lftN] in the mask of the Q-to-P view
shift, we cannot turn [†κ'] into [†κ]. *)
Parameter bor_acc_strong : E q κ P, lftN E
lft_ctx - &{κ} P - q.[κ] ={E}= κ', κ κ' P
Q, ( Q - [†κ'] ={lft_userN}= P) - Q ={E}= &{κ'} Q q.[κ].
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