“！=<”之类的错误在agda中是什么意思以及如何修复

Question

我在http://agda.readthedocs.io/en/v2.5.3/ 上找不到关于此的信息，在“agda 中的验证编程”一书中也找不到。这是什么意思？我在哪里可以了解更多类似此错误的信息？

完整的错误是.cter !=< cter of type Set

代码有点难懂，如果需要我会在稍后发布，这是关于实现模拟退火算法的。

Answer 1

字面意思是.cter 不是cter 的子类型。由于在 Agda 中对子类型的支持非常有限，这很可能意味着 Agda 期望 .cter 和 cter 相等，但事实并非如此。特别是，cter 是您代码中的一个（可见）变量，而 .cter 是 Agda 引入的一个隐藏参数，并且恰好具有相同的名称。

我希望这会有所帮助。没有看到代码很难说得更具体，所以如果你仍然卡住，请尝试找到一个有相同问题的小例子并在这里发布。