module Syntax.Decimal_Naturals where

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`

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

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

```
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
```

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 the `ℕ`

, `zero`

, and `suc`

definitions with decimal notation from the Standard Libraries:

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

(Import declarations will be discussed later.)