repos / jolie.agda.git

Network.agda

 1module Network where
 2
 3open import Data.List using (List; []; [_]; _++_)
 4open import Type
 5open import Service
 6
 7
 8data Network : Set where
 9  [_]_ : Service → Location → Network
10  νr : Network → Network
11  _∥_ : Network → Network → Network
12  nil : Network
13
14locs : Network → List Location
15locs (νr n) = locs n
16locs (n₁ ∥ n₂) = locs n₁ ++ locs n₂
17locs nil = []
18locs ([ s ] l) = [ l ]