Church numeral

Tools: Rocq (formerly Coq)

• (Semantics, Lambda calculus) Church's encoding of numbers used in Pure/Untyped lambda calculus.

Encoding: $c_n = \lambda a.\ \lambda z.\ \underbrace{a\ (a\ (\cdots (a}_{n}\ z)\cdots))$.