How does the Prelude allow numeric literals for Nat?

Question

In Type-Driven Development with Idris ch. 4, they say

The Prelude also defines functions and notation to allow Nat to be used like any other numeric type, so rather than writing S (S (S (S Z))), you can simply write 4.

and similarly for Fin. How does it achieve that? I've looked at the source but I can't figure it out.

Answer 1

from where you linked notice fromIntegerNat:

||| Convert an Integer to a Nat, mapping negative numbers to 0
fromIntegerNat : Integer -> Nat
fromIntegerNat 0 = Z
fromIntegerNat n =
  if (n > 0) then
    S (fromIntegerNat (assert_smaller n (n - 1)))
  else
    Z

and fromInteger in the Num implementation of Nat:

Num Nat where
  (+) = plus
  (*) = mult

  fromInteger = fromIntegerNat

and Cast Integer Nat

||| Casts negative `Integers` to 0.
Cast Integer Nat where
  cast = fromInteger

In the case of Idris1 it will attempt to cast from a literal (such as Char, String or Integer) into whatever type is required via those "fromFunctions" (as noted in a comment in one of the above sources: [...] '-5' desugars to 'negate (fromInteger 5)') and in general Idris1 supports implicit casting for any two types. ( http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit-conversions )

In the case of Idris2, there are some pragmas (%charLit fromChar, %stringLit fromString, %integerLit fromInteger) to hint the compiler to use some cast function from a literal into any other type.