重载字面量

编译器提供了字面量重载的指令，分别是字符串字面量的 %stringLit <fun> 和整数字面量的 %integerLit <fun>。在细化阶段，给定的函数会被应用到相应的字面量上。在 Prelude 中，这些函数被设置为 fromString 和 fromInteger。

接口 FromString ty 提供了 fromString : String -> ty 函数，而 Num ty 接口为所有数值类型提供了 fromInteger : Integer -> ty 函数。

受限重载

虽然字面量重载可以通过实现上述接口来实现，但原则上只需要一个具有正确签名和名称的函数就足以实现所需的行为。这可以用来获得更严格的重载，例如将字面量转换为 Fin n 值，其中大于或等于 n 的整数字面量不是该类型的可构造值。可以在函数签名中添加额外的隐式参数，特别是用于搜索证明的自动隐式参数。例如，这是 Fin n 的 fromInteger 实现。

public export
fromInteger : (x : Integer) -> {n : Nat} ->
              {auto prf : (IsJust (integerToFin x n))} ->
              Fin n
fromInteger {n} x {prf} with (integerToFin x n)
  fromInteger {n} x {prf = ItIsJust} | Just y = y

prf 自动隐式参数是一个自动构造的证明（如果可能的话），证明该字面量适合 Fin n 类型。这种受限行为可以在 REPL 中观察到，其中构造有效证明的失败会在类型检查阶段而不是运行时被捕获：

Main> the (Fin 3) 2
FS (FS FZ)
Main> the (Fin 3) 5
(interactive):1:13--1:14:Can't find an implementation for IsJust (integerToFin 5 3) at:
1   the (Fin 3) 5