Solution (source code)

= Solution

The function is the <predecessor function>. It has the <primitive recursion> definition
$$
f(0)=0,
\qquad
f(n+1)=n.
$$
The initial function is the zero function and the recursion step is a projection function, both of which are <primitive recursive functions>. Closure under primitive recursion therefore proves that $f$ is primitive recursive.