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.\underset{n}{\underbrace{a(a(\cdots (a}}z)\cdots ))$.