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

module SVDesc where

open import NeilPrelude

---------------------------------------------------------

infixr  _,_

data SVDesc : Set where
  C   : Set → SVDesc
  E   : Set → SVDesc
  S   : Set → SVDesc
  _,_ : SVDesc → SVDesc → SVDesc

---------------------------------------------------------

Sample : SVDesc → Set
Sample (C A)      = A
Sample (E A)      = Maybe A
Sample (S A)      = A
Sample (as , bs)  = Sample as × Sample bs

---------------------------------------------------------