Natural numbers and vectors and such

Utils.hs

{-# LANGUAGE UnicodeSyntax, NoStarIsType, LambdaCase #-}
{-# LANGUAGE GADTs, DataKinds, PolyKinds, PatternSynonyms, ViewPatterns, TypeApplications #-}

module Utils where

import Data.Kind

-- The usual definitions of Nat and Vec:
data Nat = Z | S Nat

data Vec :: Nat -> Type -> Type where
  VNil :: Vec 'Z a
  (:>) :: a -> Vec n a -> Vec ('S n) a

instance Functor (Vec n) where
  fmap _ VNil = VNil
  fmap f (x:>xs) = f x :> fmap f xs