Как Prelude позволяет использовать литералы numeri c для Nat?

Question

In Типовая разработка с Idris ch. 4, они говорят

Prelude также определяет функции и обозначения, позволяющие использовать Nat как любой другой тип numeri c, поэтому вместо записи S (S (S (S Z))) вы можете просто написать 4.

и аналогично для Fin. Как этого добиться? Я просмотрел источник , но не могу понять.

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

и fromInteger в реализации Num Nat:

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

  fromInteger = fromIntegerNat

и Cast Integer Nat

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

В случае Idris1 он попытается выполнить приведение из литерала (такого как Char, String или Integer) в любой требуемый тип с помощью этих «fromFunctions» (как указано в комментарии в одном из вышеперечисленных источников: [...] '-5' desugars to 'negate (fromInteger 5)'), и в целом Idris1 поддерживает неявное приведение типов для любых двух типов. (http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit -конверсии )

В случае с Idris2 есть некоторые прагмы (%charLit fromChar, %stringLit fromString, %integerLit fromInteger) для подсказки компилятор использовать некоторую функцию приведения из литерала в любой другой тип.