Update typing rules for network and service layers.

diff --git a/src/TypingNetwork.agda b/src/TypingNetwork.agda
index ad77cc35cb5bb1509481effc3d3c96f328a6bb2f..c3d1b90f2b20f8da6c6696c438e0aa15ec77f01a 100644 (file)
--- a/src/TypingNetwork.agda
+++ b/src/TypingNetwork.agda
@@ -21,15 +21,15 @@ data _⊢N_ : Context → Network → Set where
                --------------------------
                → Γ ⊢N ([ b ▹ d - p ] l)
 
-  t-network : ∀ {n} {m} {Γ₁ : Ctx n} {Γ₂ : Ctx m} {N₁ N₂ : Network} {l : Location}
-            → ◆ Γ₁ ⊢N N₁
-            → ◆ Γ₂ ⊢N N₂
+  t-network : {Γ₁ Γ₂ : Context} {N₁ N₂ : Network} {l : Location}
+            → Γ₁ ⊢N N₁
+            → Γ₂ ⊢N N₂
 --            →  , ¬ (l ∈ fromList (locs N₁))
             → ¬ (l ∈-Vec fromList (locs N₂))
             ----------------------
-            → ■ (◆ Γ₁) (◆ Γ₂) ⊢N (N₁ ∥ N₂)
+            → & Γ₁ Γ₂ ⊢N (N₁ ∥ N₂)
 
-  t-restriction : ∀ {n} {Γ : Ctx n} {n : Network}
-                → ◆ Γ ⊢N n
+  t-restriction : {Γ : Context} {n : Network}
+                → Γ ⊢N n
                 -------------
-                → ◆ Γ ⊢N νr n
+                → Γ ⊢N νr n

diff --git a/src/TypingService.agda b/src/TypingService.agda
index efe748ff9dcc0f01409231de56c1b69c9dd42082..3953627a19f0db0618ae00c8cf621660ff10899b 100644 (file)
--- a/src/TypingService.agda
+++ b/src/TypingService.agda
@@ -20,12 +20,12 @@ data _⊢BSL_▹_ : Context → Behaviour → Context → Set where
 
   -- TODO
   t-bsl-choice : ∀ {m k} {Γ : Context} {contexts : Vec (Ctx m) k} {choices : List (η × Behaviour)} {Tₐ Tₓ : Type} {x : Variable}
-               â\86\92 All (λ { (Î\93â\82\81 , (η , b)) â\86\92 Î\93 â\8a¢B input η â\88¶ b â\96¹ â\97\86 Î\93â\82\81 }) (zip (toList contexts) choices)
-               â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\97\86 (concat contexts))
-               â\86\92 ¬ (var x Tâ\82\90 â\88\88 â\97\86 (concat contexts))
+               â\86\92 All (λ { (Î\93â\82\81 , (η , b)) â\86\92 Î\93 â\8a¢B input η â\88¶ b â\96¹ â\8b\86 Î\93â\82\81 }) (zip (toList contexts) choices)
+               â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\8b\86 (concat contexts))
+               â\86\92 ¬ (var x Tâ\82\90 â\88\88 â\8b\86 (concat contexts))
                → Tₓ ≢ Tₐ
                ----------------------------------------------
-               â\86\92 Î\93 â\8a¢BSL inputchoice choices â\96¹ â\97\86 (concat contexts)
+               â\86\92 Î\93 â\8a¢BSL inputchoice choices â\96¹ â\8b\86 (concat contexts)
 
 data _⊢state_ : Context → Process → Set where