repos / jolie.agda.git

commit

20163ca

parent

80305d1

author

Eugene Akentyev

date

2016-12-07 17:41:23 +0400 +04

Update service

 1@@ -1,5 +1,6 @@
 2 module Service where
 3 
 4+open import Data.Nat using (ℕ)
 5 open import Data.List using (List)
 6 open import Data.String using (String)
 7 open import Data.Product using (_×_)
 8@@ -22,8 +23,8 @@ data Process : Set where
 9 
10 data AliasingFunction : Set where
11 
12-Deployment : Set
13-Deployment = AliasingFunction × Γ
14+Deployment : {m : ℕ} → Set
15+Deployment {m} = AliasingFunction × Ctx m
16 
17 data Service : Set where
18-  service : Behaviour → Deployment → Process → Service
19+  service : {m : ℕ} → Behaviour → Deployment {m} → Process → Service