Skip to content

GitLab

A
Actris
Commit 6045937e authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files
Options

Added notation for telescope message types

parent e0300f5f
Hide whitespace changes
Inline Side-by-side
Showing with 6 additions and 0 deletions
theories/logrel/session_types.v
View file @ 6045937e
...@@ -50,6 +50,9 @@ Notation "<!! X .. Y > M" := ...@@ -50,6 +50,9 @@ Notation "<!! X .. Y > M" :=
(<!!> ∃ X, .. (∃ Y, M) ..)%lty (<!!> ∃ X, .. (∃ Y, M) ..)%lty
(at level 200, X closed binder, Y closed binder, M at level 200, (at level 200, X closed binder, Y closed binder, M at level 200,
format "<!! X .. Y > M") : lty_scope. format "<!! X .. Y > M") : lty_scope.
Notation "<!!.. X .. Y > M" := (<!!> ∃.. X, .. (∃.. Y, M) ..)%lty
(at level 200, X closed binder, Y closed binder, M at level 200,
format "<!!.. X .. Y > M") : lty_scope.
Notation "<??> M" := Notation "<??> M" :=
(lty_message Recv M) (at level 200, M at level 200) : lty_scope. (lty_message Recv M) (at level 200, M at level 200) : lty_scope.
...@@ -57,6 +60,9 @@ Notation "<?? X .. Y > M" := ...@@ -57,6 +60,9 @@ Notation "<?? X .. Y > M" :=
(<??> ∃ X, .. (∃ Y, M) ..)%lty (<??> ∃ X, .. (∃ Y, M) ..)%lty
(at level 200, X closed binder, Y closed binder, M at level 200, (at level 200, X closed binder, Y closed binder, M at level 200,
format "<?? X .. Y > M") : lty_scope. format "<?? X .. Y > M") : lty_scope.
Notation "<??.. X .. Y > M" := (<??> ∃.. X, .. (∃.. Y, M) ..)%lty
(at level 200, X closed binder, Y closed binder, M at level 200,
format "<??.. X .. Y > M") : lty_scope.
Notation lty_select := (lty_choice Send). Notation lty_select := (lty_choice Send).
Notation lty_branch := (lty_choice Recv). Notation lty_branch := (lty_choice Recv).
Infix "<++>" := lty_app (at level 60) : lty_scope. Infix "<++>" := lty_app (at level 60) : lty_scope.
......
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