为什么在"伊德里斯"中不涉及"mod"的平等不是类型检查？

Question

为什么不会出现以下类型的问题:

v1 : mod 3 2 = 1
v1 = Refl

然而,这将很好地检查:

v2 : 3 - 2 = 1
v2 = Refl

Answer 1

这是由于mod功能的偏倚(感谢@AntonTrunov澄清).它是多态的,默认数字常量是Integers.

Idris> :t mod
mod : Integral ty => ty -> ty -> ty
Idris> :t 3
3 : Integer
Idris> :t mod 3 2
mod 3 2 : Integer

对于Integer类型mod功能不是全部.

而是使用modNatNZ功能,所以所有类型检查完美和工作.

v1 : modNatNZ 3 2 SIsNotZ = 1
v1 = Refl