module exampleMapAppliedToList where


data N : Set where 
  Z : N
  S : N -> N

{-# BUILTIN NATURAL  N  #-}
{-# BUILTIN ZERO     Z    #-}
{-# BUILTIN SUC      S    #-}





data NatList : Set where
  nil : NatList
  cons : N -> NatList -> NatList

map : (N -> N) -> NatList -> NatList
map f nil        = nil
map f (cons n l') = cons (f n) (map f l')

test : NatList
test = map S (cons 2 (cons 3 nil))


{- A better notation for NatList is as follows -}

data NatList' : Set where
  [] : NatList'
  _::_ : N -> NatList' -> NatList'

infixr 50 _::_


map' : (N -> N) -> NatList' -> NatList'
map' f []        = []
map' f (n :: l') = f n :: map' f l'

test' : NatList'
test' = map' S (2 :: 3 :: 4 :: [])