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

【问题标题】：How does the Prelude allow numeric literals for Nat?Prelude 如何允许 Nat 使用数字文字？
【发布时间】：2020-08-19 13:13:18
【问题描述】：

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

Prelude 还定义了函数和符号，以允许 Nat 像任何其他数字类型一样使用，因此您可以简单地编写 4，而不是编写 S (S (S (S Z)))。

同样适用于Fin。它是如何做到这一点的？我看过the source，但我无法弄清楚。

【问题讨论】：

标签： idris syntactic-sugar

【解决方案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在Nat的Num实现中：

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

  fromInteger = fromIntegerNat

并转换整数 Nat

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

在 Idris1 的情况下，它将尝试通过“fromFunctions”从文字（例如 Char、String 或 Integer）转换为所需的任何类型（如上述来源之一的评论中所述：@987654328 @) 并且通常 Idris1 支持任何两种类型的隐式转换。 (http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit-conversions)

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

【讨论】：