From 80b8d62649942f6ec9ea33260e71b7db6bdf5f3c Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 11 Jun 2019 18:28:01 +0200
Subject: [PATCH] Added notation for branching
---
theories/encodings/branching.v | 6 +++++-
theories/examples/branching_examples.v | 6 +++---
2 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/theories/encodings/branching.v b/theories/encodings/branching.v
index 44a0eb4..4bdf43c 100644
--- a/theories/encodings/branching.v
+++ b/theories/encodings/branching.v
@@ -90,4 +90,8 @@ Section branching_specs.
- wp_pures. iApply ("HΦ'"). eauto with iFrame.
Qed.
-End branching_specs.
\ No newline at end of file
+End branching_specs.
+
+Notation "'branch:' c @ s 'left' e1 'right' e2" :=
+ (branch c s (λ: <>, e1)%E (λ: <>, e2)%E #())
+ (at level 200, c, s, e1, e2 at level 200) : expr_scope.
diff --git a/theories/examples/branching_examples.v b/theories/examples/branching_examples.v
index 327ecfd..bd75583 100644
--- a/theories/examples/branching_examples.v
+++ b/theories/examples/branching_examples.v
@@ -11,9 +11,9 @@ Section BranchingExamples.
Definition branch_example b : expr :=
(let: "c" := new_chan #() in
select "c" #Left #b;;
- Fork((branch "c" #Right
- (λ: <>, send "c" #Right #5)
- (λ: <>, #())) #());;
+ Fork(branch: "c" @ #Right
+ left send "c" #Right #5
+ right #());;
(if: #b then recv "c" #Left else #()))%E.
End BranchingExamples.
\ No newline at end of file
--
GitLab