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]