Skip to content

Instantly share code, notes, and snippets.

@copumpkin

copumpkin/Ack.agda

Created June 2, 2015 01:41
Show Gist options
  • Save copumpkin/6677ba1bb6353b51c543 to your computer and use it in GitHub Desktop.
Save copumpkin/6677ba1bb6353b51c543 to your computer and use it in GitHub Desktop.
Download ZIP
Ackermann
Raw
Ack.agda
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment