为什么涉及“mod”的平等不会在Idris中进行类型检查？

v2 : 3 - 2 = 1 
v2 = Refl

2017-06-21 redfish64

它发生：

v1 : mod 3 2 = 1 
v1 = Refl

然而，这将类型检查，罚款。它是多态的，默认数字常量是Integer s。

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

对于Integermod类型的功能是不总。

取而代之的是使用modNatNZ函数，因此所有类型的检测都是完美无缺的，并且工作正常。

v1 : modNatNZ 3 2 SIsNotZ = 1 
v1 = Refl

2017-06-21 12:21:49 Shersh

恐怕“在编译器阶段Idris只能在类型中执行模式匹配”这句话是不正确的。举个例子，'（Int 3） - 2 = 1'，你可以用'Refl'来证明它，尽管'Int'不是一个归纳数据类型。正如你已经解释过的，'Refl'不能用'mod'的原因是偏袒的。 –

回答