- commit
- 84fbee9
- parent
- eb93f60
- author
- Eugene Akentyev
- date
- 2017-01-26 11:22:16 +0400 +04
Cosmetic changes
1 files changed,
+5,
-0
+5,
-0
1@@ -80,21 +80,26 @@ data _↝_∶_ : Behaviour → Behaviour → Label → Set where
2
3 b-if-then : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
4 → e ⟨ t ⟩≔ (constant (bool true))
5+ -----------------------------------------
6 → (if e then b₁ else b₂) ↝ b₁ ∶ lb-read t
7
8 b-if-else : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
9 → e ⟨ t ⟩≔ (constant (bool false))
10+ -----------------------------------------
11 → (if e then b₁ else b₂) ↝ b₂ ∶ lb-read t
12
13 b-iteration : {e : Expr} {t : State} {b : Behaviour}
14 → e ⟨ t ⟩≔ (constant (bool true))
15+ ---------------------------------------------------
16 → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ lb-read t
17
18 b-no-iteration : {e : Expr} {t : State} {b : Behaviour}
19 → e ⟨ t ⟩≔ (constant (bool false))
20+ ----------------------------------
21 → (while[ e ] b) ↝ nil ∶ lb-read t
22
23 b-choice : ∀ {n} {choices : Vec (η × Behaviour) n} {ηⱼ : η} {η : Label} {bⱼ bⱼ′ : Behaviour}
24 → (ηⱼ , bⱼ) ∈-Vec choices
25 → input ηⱼ ↝ bⱼ′ ∶ η
26+ ----------------------------------------------
27 → inputchoice (toList choices) ↝ (bⱼ′ ∶ bⱼ) ∶ η