{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude
open import Bool

module Descriptors where

open import List public


-- Decoupledness Descriptors -- 

-- Rather than create a datatype for Dec, we use booleans so we can use existing
-- boolean proofs

Dec : Set
Dec = Bool

dec : Dec
dec = false

cau : Dec
cau = true


-- Signal Descriptors --

data SigDesc : Set where
  E : Set → SigDesc
  C : Set → SigDesc

SVDesc : Set
SVDesc = List SigDesc