module Syntax.Decimal_Naturals where

Constants in Peano Representation

Peano representation of natural number constants which are greater than three are hard to read:

suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))

On the other hand, decimal representation which we are used to is easy to read:

12

Decimal notation for Peano representation

Agda's solution is to keep the Peano representation while giving a decimal notation for constants in Peano representation.

For example,

3

will be a shorthand for

suc (suc (suc zero))

Technical details

Agda needs special directives to allow decimal notations of constants in Peano representation:

data ℕ : Set where
  zero :     ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

Unfortunately, this BUILTIN machinery is not designed to accommodate multiple definitions of a given BUILTIN. If we wish to use definitions from the Standard Libraries later (and we wish), we cannot make another Peano representation of naturals with decimal notation.

The solution is to reuse the existing ℕ, zero, suc definitions with decimal notation from the Standard Libraries:

open import Data.Nat public using (ℕ; zero; suc)

(import declarations are discussed later.)