Skip to content

Instantly share code, notes, and snippets.

@copumpkin copumpkin/Ack.agda
Created Jun 2, 2015

Embed
What would you like to do?
Ackermann
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
You can’t perform that action at this time.