module Padova2025.ProgrammingBasics.Naturals.Base where

Definition

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

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))).