Prelude如何允许Nat使用数字文字？

Question

在使用Idris进行类型驱动的开发中 ch。 4，他们说

The Prelude还定义了功能和表示法，以允许像使用任何其他数字类型一样使用Nat，因此除了编写S (S (S (S Z)))，您还可以简单地编写4。

[对于Fin同样。它是如何实现的？我看过the source，但无法弄清楚。

Answer 1

链接通知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

和Nat的Num实现中的fromInteger：
Num Nat where
  (+) = plus
  (*) = mult

  fromInteger = fromIntegerNat

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

对于Idris1，它将尝试通过那些“ fromFunctions”将文字（如Char，String或Integer）转换为所需的任何类型（如上述来源之一的注释中所述：[...] '-5' desugars to否定（fromInteger 5）`），并且通常Idris1支持任意两种类型的隐式转换。 （http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit-conversions）
对于Idris2，有一些pragmas（%charLit fromChar，%stringLit fromString，%integerLit fromInteger）来提示编译器使用一些从文字转换为其他类型的转换函数。