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

Changed <++++> to an overload of <++>

parent 8a7a8f7c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/logrel/session_types.v
+ 1
− 1
View file @ 5c2891ce
...@@ -95,4 +95,4 @@ Notation "<!!> A ; P" := ...@@ -95,4 +95,4 @@ Notation "<!!> A ; P" :=
(lsty_send A P) (at level 20, A, P at level 200) : lsty_scope. (lsty_send A P) (at level 20, A, P at level 200) : lsty_scope.
Notation "<??> A ; P" := Notation "<??> A ; P" :=
(lsty_recv A P) (at level 20, A, P at level 200) : lsty_scope. (lsty_recv A P) (at level 20, A, P at level 200) : lsty_scope.
Infix "<++++>" := lsty_app (at level 60) : lsty_scope. Infix "<++>" := lsty_app (at level 60) : lsty_scope.
theories/logrel/subtyping.v
+ 1
− 1
View file @ 5c2891ce
...@@ -285,7 +285,7 @@ Section subtype. ...@@ -285,7 +285,7 @@ Section subtype.
Lemma lsty_app_le P11 P12 P21 P22 : Lemma lsty_app_le P11 P12 P21 P22 :
(P11 <p: P21) -∗ (P12 <p: P22) -∗ (P11 <p: P21) -∗ (P12 <p: P22) -∗
(P11 <++++> P12) <p: (P21 <++++> P22). (P11 <++> P12) <p: (P21 <++> P22).
Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed. Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
Lemma lsty_dual_le P1 P2 : P2 <p: P1 -∗ lsty_dual P1 <p: lsty_dual P2. Lemma lsty_dual_le P1 P2 : P2 <p: P1 -∗ lsty_dual P1 <p: lsty_dual P2.
......
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