module Padova2025.ProgrammingBasics.Naturals.Base where
Definition
In the previous chapter, we have defined the finite type of Booleans. Agda also supports infinite types. The natural numbers are the primordial example, and we will explore them now. The type of natural numbers is brought into existence with the following three lines of Agda code.
data ℕ : Set where -- enter "ℕ" by "\bN" zero : ℕ succ : ℕ → ℕ -- short for "successor"
The succ constructor outputs, for each input, a new
freshly-minted value of the type ℕ. Hence the type
ℕ contains the following distinct elements:
-- zero -- succ zero -- succ (succ zero) -- succ (succ (succ zero)) -- ...
We can define abbreviations for often-occuring numbers:
one : ℕ one = succ zero two : ℕ two = succ one three : ℕ three = succ two four : ℕ four = succ three five : ℕ five = succ four
Writing natural numbers in unary is a pain. By adding
{-# BUILTIN NATURAL ℕ #-} on a line of its own, we can ask
Agda to enable suitable syntactic sugar. From then on, we can write
decimal expressions like 42 which Agda will transparently
desugar to appropriate succ calls:
succ (succ (... (zero))).