English
The code for the partially applied Ackermann function.
Русский
Код частично применённой функции Аккермана.
LaTeX
$$$$pappAck : \\mathbb{N} \\to Code.$$$$
Lean4
/-- The code for the partially applied Ackermann function.
This is used to prove that the Ackermann function is computable. -/
def pappAck : ℕ → Code
| 0 => .succ
| n + 1 => step (pappAck n)
where/-- Yields single recursion step on `pappAck`. -/
step (c : Code) : Code := .curry (.prec (.comp c (.const 1)) (.comp c (.comp .right .right))) 0