# Definition:Basic Primitive Recursive Function/Successor Function

## Definition

The successor function $\Succ: \N \to \N$ is a basic primitive recursive function, defined as:

$\forall n \in \N: \map \Succ n = n + 1$