Skip to content

Instantly share code, notes, and snippets.

@copumpkin

copumpkin/Ack.agda

Created June 2, 2015 01:41
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save copumpkin/6677ba1bb6353b51c543 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save copumpkin/6677ba1bb6353b51c543 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. copumpkin created this gist Jun 2, 2015.
    17 changes: 17 additions & 0 deletions Ack.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,17 @@
    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)