Commit 821a4c23 authored by Jonas Kastberg's avatar Jonas Kastberg

Whitespace cleanup

parent eb01938a
...@@ -500,12 +500,12 @@ Section properties. ...@@ -500,12 +500,12 @@ Section properties.
- wp_apply "Hv2". iApply "Hc2". - wp_apply "Hv2". iApply "Hc2".
- iIntros (w1 w2) "[Hw1 Hw2]". - iIntros (w1 w2) "[Hw1 Hw2]".
iSplitL "Hw1 Hw2". iSplitL "Hw1 Hw2".
+ iExists _, _. iFrame. done. + iExists _, _. iFrame. done.
+ iApply "Hsplit2". iFrame "HΓ1' HΓ2'". + iApply "Hsplit2". iFrame "HΓ1' HΓ2'".
Qed. Qed.
End with_spawn. End with_spawn.
Lemma ltyped_send Γ Γ' (x : string) e A S : Lemma ltyped_send Γ Γ' (x : string) e A S :
Γ' !! x = Some (chan (<!!> TY A; S))%lty Γ' !! x = Some (chan (<!!> TY A; S))%lty
(Γ e : A Γ') - (Γ e : A Γ') -
......
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