为什么Agda给出错误"expected:ℕ，actual:ℕ“
为什么Agda给出错误"expected:ℕ，actual:ℕ“
提问于 2018-06-07 22:47:28
当我写下面的函数是agda时，
f : (A : Set) → (a : A) → ℕ
f ℕ n = n我希望错误提示我没有指定所有的情况。
相反，我得到了这个错误：
Type mismatch:
expected: ℕ
actual: ℕ
when checking that the expression n
has type ℕ这里发生什么事情？
回答 1
Stack Overflow用户
回答已采纳
发布于 2018-06-08 05:17:32
使用较新版本的Agda (我使用的是2.5.4)，您会得到一个更具信息性的错误：
ℕ !=< ℕ of type Set
(because one is a variable and one a defined identifier)
when checking that the expression n has type ℕ问题是函数定义的模式(在等号的左边)只能包含构造函数、变量和点模式，而不能包含ℕ之类的类型。由于ℕ不是一个有效的模式，Agda假定它是一个名为ℕ的Set类型的新变量，从而掩盖了自然数的实际类型ℕ。现在这个错误是有意义的，因为n的类型(即变量的ℕ )不等于预期的返回类型(即自然数的ℕ类型)。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/50744196
复制相关文章
相似问题