我在http://agda.readthedocs.io/en/v2.5.3/上找不到这方面的信息，在“agda验证编程”一书上也找不到。这是什么意思？我在哪里可以知道更多像这样的错误？
完全错误是.cter !=< cter of type Set
这段代码有点错误，所以如果需要的话，我会稍后发布，这是关于实现模拟退火算法的。
最佳答案
字面意思是.cter不是cter的子类型由于在agda中对子类型的支持非常有限，这很可能意味着agda期望.cter和cter相等，但事实并非如此。特别是，cter是代码中的一个（可见）变量，而.cter是agda引入的一个隐藏参数，并且碰巧具有相同的名称。
我希望这能有帮助。不看代码很难更具体，所以如果你仍然被困，请试着找到一个有相同问题的小例子，并张贴在这里。
关于algorithm - 错误(!= <)在Agda中的含义是什么，以及如何解决，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/49005563/