module DepType
  
import Data.Fin

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
  
sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False (x :: xs) = x + sum False xs

data MyVect : Nat -> Type -> Type where
  Nil : MyVect Z a
  (::) : a -> MyVect k a -> MyVect (S k) a

(++) : MyVect k a -> MyVect l a -> MyVect (k + l) a
(++) [] ys = ys
(++) (x :: xs) ys = x :: xs ++ ys

length : MyVect n a -> Nat
length xs {n} = n