7ML7W Idris Days 1 2

-- A function which takes a value and a list, and returns a
-- list of all elements in the original list greater than the
-- value. We used `Ord` to allow the function to take any type
-- that is "orderable", so characters work as well as numbers
greaterThan : Ord a => a -> List a -> List a
greaterThan v = filter ( > v )

-- Return every other item in the list, starting with the
-- first one
everyOther : List a -> List a
everyOther [] = []
everyOther [x] = [x]
everyOther (x :: y :: rest) = x :: everyOther rest

-- A Vector of a specific size containing members of a specific type
data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

-- Our attempt at defining a function which only adds vectors of
-- the same size
(++) : Vect n a -> Vect n a -> Vect (n + n) a
(++) Nil Nil = Nil
(++) (x :: xs) (y :: ys) = x :: y :: (xs ++ ys)