open import Agda.Builtin.List using (List; []; _∷_)
open import Agda.Builtin.Nat using (Nat; _+_)

sum : List Nat → Nat
sum [] = 
sum (x ∷ xs) = x + sum xs

pattern [_⨾_] x y = x ∷ y ∷ []

testSum : Nat
testSum = sum [  ⨾  ]

private variable A B C : Set

_++_ : List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

map : (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

zipWith : (A → B → C) → List A → List B → List C
zipWith f []       _        = []
zipWith f _        []       = []
zipWith f (a ∷ as) (b ∷ bs) = f a b ∷ zipWith f as bs

open import Agda.Builtin.Nat

test : Nat
test =  + testSum
         + sum ( ∷  ∷ [])
         + sum (map suc ( ∷  ∷ []))
         + sum (zipWith _+_ ( ∷ []) ( ∷ []))
{-# COMPILE AGDA2LAMBOX test #-}