From 84fbee90e160375638ee76ab14a9d2513ca6a992 Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Thu, 26 Jan 2017 10:22:16 +0300
Subject: [PATCH] Cosmetic changes

---
 src/BehaviouralSemantics.agda | 5 +++++
 1 file changed, 5 insertions(+)

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ⱼ) ∶ η
-- 
2.50.1