## 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`:

```{-# 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 `Fin n` can then be defined as follows:

```data IsTrue : Bool → Set where
itis : IsTrue true

instance
indeed : IsTrue true
indeed = itis

_<?_ : Nat → Nat → Bool
zero <? zero = false
zero <? suc y = true
suc x <? zero = false
suc x <? suc y = x <? y

natToFin : ∀ {n} (m : Nat) {{_ : IsTrue (m <? n)}} → Fin n
natToFin {zero} zero {{()}}
natToFin {zero} (suc m) {{()}}
natToFin {suc n} zero {{itis}} = zero
natToFin {suc n} (suc m) {{t}} = suc (natToFin m)

instance
NumFin : ∀ {n} → Number (Fin n)
Number.Constraint (NumFin {n}) k = IsTrue (k <? n)
Number.fromNat    NumFin       k = natToFin k
```

## 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 #-}
```

## Other types¶

Currently only integer and string literals can be overloaded.