13 lines
241 B
Agda
13 lines
241 B
Agda
|
open import Data.Nat
|
|||
|
|
open import Data.Nat.Show
|
|||
|
|
open import IO
|
|||
|
|
|
|||
|
|
module Ackermann where
|
|||
|
|
|
|||
|
|
ack : ℕ -> ℕ -> ℕ
|
|||
|
|
ack zero n = n + 1
|
|||
|
|
ack (suc m) zero = ack m 1
|
|||
|
|
ack (suc m) (suc n) = ack m (ack (suc m) n)
|
|||
|
|
|
|||
|
|
main = run (putStrLn (show (ack 3 9)))
|