Cosmetic changes

diff --git a/src/BehaviouralSemantics.agda b/src/BehaviouralSemantics.agda
index cbc55ad8e9bd22456e3e08e763da59427e338de6..276d93c02c18f001df4c967fce5a7d7acd29fd24 100644 (file)
--- 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ⱼ) ∶ η