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

Rewrite Nits

parent 1be0cae7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/channel/proto.v
+ 6
− 6
View file @ a7db0dc2
......@@ -772,13 +772,13 @@ Section proto.
iMod (iProto_le_end_inv_l with "H") as "H".
rewrite iProto_end_eq iProto_message_eq.
iDestruct (proto_message_end_equivI with "H") as "[]".
- rewrite -> Heq. destruct a.
- iEval (rewrite Heq). destruct a.
+ iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=".
iDestruct "Hm1" as (x) "Hm1".
iSpecialize ("H" $! x). rewrite -> Heq.
iSpecialize ("H" $! x). rewrite Heq.
iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
+ iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
iSpecialize ("H" $! x). rewrite -> Heq.
iSpecialize ("H" $! x). rewrite Heq.
by iApply (iProto_le_recv_recv_inv with "H").
Qed.
......@@ -804,13 +804,13 @@ Section proto.
iMod (iProto_le_end_inv_r with "H") as "H".
rewrite iProto_end_eq iProto_message_eq.
iDestruct (proto_message_end_equivI with "H") as "[]".
- rewrite -> Heq. destruct a.
- iEval (rewrite Heq). destruct a.
+ iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
iSpecialize ("H" $! x). rewrite -> Heq.
iSpecialize ("H" $! x). rewrite Heq.
by iApply (iProto_le_send_send_inv with "H").
+ iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1".
iDestruct 1 as (x) "Hm2".
iSpecialize ("H" $! x). rewrite -> Heq.
iSpecialize ("H" $! x). rewrite Heq.
iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
Qed.
Lemma iProto_le_exist_intro_l {A} (m : A → iMsg Σ V) a :
......
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