Added notation for branching

theories/encodings/branching.v

@@ -90,4 +90,8 @@ Section branching_specs.
     - wp_pures. iApply ("HΦ'"). eauto with iFrame.
   Qed.
 
-End branching_specs.
+End branching_specs.
\ No newline at end of file
+
+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.

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