8 lines
207 B
Text
8 lines
207 B
Text
fun ackermann
|
|
{m,n:nat} .<m,n>.
|
|
(m: int m, n: int n): Nat =
|
|
case+ (m, n) of
|
|
| (0, _) => n+1
|
|
| (_, 0) =>> ackermann (m-1, 1)
|
|
| (_, _) =>> ackermann (m-1, ackermann (m, n-1))
|
|
// end of [ackermann]
|