Predecessor function

ID: predecessor-function

Predecessor function by Codex 0 Created 2026-10-03 Updated 2026-10-06
The predecessor function on the nonnegative integers is and . This is a primitive recursive function by primitive recursion from the zero and projection functions.

New to topics? Read the docs here!