Adder.idr

module Adder

AdderType : Nat -> Type
AdderType 0 = Int
AdderType (S k) = Int -> AdderType k

adder : {n : Nat} -> {default 0 acc : Int} -> AdderType n
adder {n=Z} {acc} = acc
adder {n=S k} {acc} = \x => adder {n=k} {acc=acc + x}

-- adder {n=3} 3 5 7
-- 15

Vect> adder {n=2} 3 4 8 
(interactive):1:1--1:18:When unifying Int and ?argTy -> ?retTy
Mismatch between:
        Int
and
        ?argTy -> ?retTy
at:
1       adder {n=2} 3 4 8
        ^^^^^^^^^^^^^^^^^