From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Thu, 26 Jan 2017 07:22:16 +0000 (+0300)
Subject: Cosmetic changes
X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=84fbee90e160375638ee76ab14a9d2513ca6a992;p=jolie.agda.git

Cosmetic changes
---

diff --git a/src/BehaviouralSemantics.agda b/src/BehaviouralSemantics.agda
index cbc55ad..276d93c 100644
--- a/src/BehaviouralSemantics.agda
+++ b/src/BehaviouralSemantics.agda
@@ -80,21 +80,26 @@ data _↝_∶_ : Behaviour → Behaviour → Label → Set where
 
   b-if-then : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
             → e ⟨ t ⟩≔ (constant (bool true))
+            -----------------------------------------
             → (if e then b₁ else b₂) ↝ b₁ ∶ lb-read t
 
   b-if-else : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
             → e ⟨ t ⟩≔ (constant (bool false))
+            -----------------------------------------
             → (if e then b₁ else b₂) ↝ b₂ ∶ lb-read t
 
   b-iteration : {e : Expr} {t : State} {b : Behaviour}
               → e ⟨ t ⟩≔ (constant (bool true))
+              ---------------------------------------------------
               → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ lb-read t
 
   b-no-iteration : {e : Expr} {t : State} {b : Behaviour}
                  → e ⟨ t ⟩≔ (constant (bool false))
+                 ----------------------------------
                  → (while[ e ] b) ↝ nil ∶ lb-read t
 
   b-choice : ∀ {n} {choices : Vec (η × Behaviour) n} {ηⱼ : η} {η : Label} {bⱼ bⱼ′ : Behaviour}
            → (ηⱼ , bⱼ) ∈-Vec choices
            → input ηⱼ ↝ bⱼ′ ∶ η
+           ----------------------------------------------
            → inputchoice (toList choices) ↝ (bⱼ′ ∶ bⱼ) ∶ η