The primitive recursive functions ℕ → ℕ.

A primcodable type is an encodable type for which the encode/decode functions are primitive recursive.

primrec f means f is primitive recursive (after encoding its input and output as natural numbers).

primrec₂ f means f is a binary primitive recursive function. This is technically unnecessary since we can always curry all the arguments together, but there are enough natural two-arg functions that it is convenient to express this directly.

primrec_pred p means p : α → Prop is a (decidable) primitive recursive predicate, which is to say that to_bool ∘ p : α → bool is primitive recursive.

primrec_rel p means p : α → β → Prop is a (decidable) primitive recursive relation, which is to say that to_bool ∘ p : α → β → bool is primitive recursive.

An alternative inductive definition of primrec which does not use the pairing function on ℕ, and so has to work with n-ary functions on ℕ instead of unary functions. We prove that this is equivalent to the regular notion in to_prim and of_prim.