-- pass parameters in bulk to types and functions

module ParameterisedBlocks

import Data.Vect

parameters (x: Nat, y : Nat) 
  addAll : Nat -> Nat
  addAll z = x + y + z

parameters (y : Nat, xs : Vect x a)
  data Vects : Type -> Type where
    MkVects : Vect y a -> Vects a

  append : Vects a -> Vect (x + y) a
  append (MkVects ys) = xs ++ ys



