module Ack where

-- http://en.wikipedia.org/wiki/Ackermann_function#Definition_and_properties

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

iterate : (Nat → Nat) → Nat → Nat
iterate f zero    = f (suc zero)
iterate f (suc n) = f (iterate f n)

ackermann : Nat → Nat → Nat
ackermann zero = suc
ackermann (suc n) = iterate (ackermann n)