## Natural numbers¶

By default natural number literals are mapped to the built-in natural number type. This can be changed with the `FROMNAT` built-in, which binds to a function accepting a natural number:

```{-# BUILTIN FROMNAT fromNat #-}
```

This causes natural number literals `n` to be desugared to `fromNat n`. Note that the desugaring happens before implicit argument are inserted so `fromNat` can have any number of implicit or instance arguments. This can be exploited to support overloaded literals by defining a type class containing `fromNat`:

```module number-simple where

record Number {a} (A : Set a) : Set a where
field fromNat : Nat → A

open Number {{...}} public
```
```{-# BUILTIN FROMNAT fromNat #-}
```

This definition requires that any natural number can be mapped into the given type, so it won’t work for types like `Fin n`. This can be solved by refining the `Number` class with an additional constraint:

```record Number {a} (A : Set a) : Set (lsuc a) where
field
Constraint : Nat → Set a
fromNat : (n : Nat) {{_ : Constraint n}} → A

open Number {{...}} public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}
```

This is the definition used in `Agda.Builtin.FromNat`. A `Number` instance for `Nat` is simply this:

```instance
NumNat : Number Nat
NumNat .Number.Constraint _ = ⊤
NumNat .Number.fromNat    m = m
```

A `Number` instance for `Fin n` can be defined as follows:

```_≤_ : (m n : Nat) → Set
zero  ≤ n     = ⊤
suc m ≤ zero  = ⊥
suc m ≤ suc n = m ≤ n

fromN≤ : ∀ m n → m ≤ n → Fin (suc n)
fromN≤ zero    _       _  = zero
fromN≤ (suc _) zero    ()
fromN≤ (suc m) (suc n) p  = suc (fromN≤ m n p)

instance
NumFin : ∀ {n} → Number (Fin (suc n))
NumFin {n} .Number.Constraint m         = m ≤ n
NumFin {n} .Number.fromNat    m {{m≤n}} = fromN≤ m n m≤n

test : Fin 5
test = 3
```

It is important that the constraint for literals is trivial. Here, `3 ≤ 5` evaluates to `⊤` whose inhabitant is found by unification.

Using predefined function from the standard library and instance `NumNat`, the `NumFin` instance can be simply:

```open import Data.Fin using (Fin; #_)
open import Data.Nat using (suc; _≤?_)
open import Relation.Nullary.Decidable using (True)

instance
NumFin : ∀ {n} → Number (Fin n)
NumFin {n} .Number.Constraint m         = True (suc m ≤? n)
NumFin {n} .Number.fromNat    m {{m<n}} = #_ m {m<n = m<n}
```

## Negative numbers¶

Negative integer literals have no default mapping and can only be used through the `FROMNEG` built-in. Binding this to a function `fromNeg` causes negative integer literals `-n` to be desugared to `fromNeg n`, where `n` is a built-in natural number. From `Agda.Builtin.FromNeg`:

```record Negative {a} (A : Set a) : Set (lsuc a) where
field
Constraint : Nat → Set a
fromNeg : (n : Nat) {{_ : Constraint n}} → A

open Negative {{...}} public using (fromNeg)
{-# BUILTIN FROMNEG fromNeg #-}
```

## Strings¶

String literals are overloaded with the `FROMSTRING` built-in, which works just like `FROMNAT`. If it is not bound string literals map to built-in strings. From `Agda.Builtin.FromString`:

```record IsString {a} (A : Set a) : Set (lsuc a) where
field
Constraint : String → Set a
fromString : (s : String) {{_ : Constraint s}} → A

open IsString {{...}} public using (fromString)
{-# BUILTIN FROMSTRING fromString #-}
```

## Restrictions¶

Currently only integer and string literals can be overloaded.