Prelude 如何允许 Nat 的数字文字？

Question

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

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.

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 'negate (fromInteger 5)') 通常 Idris1 支持任何两种类型的隐式转换。 ( http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit-conversions )

在 Idris2 的情况下，有一些 pragmas（%charLit fromChar、%stringLit fromString、%integerLit fromInteger）提示编译器从文字中使用一些强制转换函数转换成任何其他类型。

Prelude 如何允许 Nat 的数字文字？

How does the Prelude allow numeric literals for Nat?

syntactic-sugar

idris