Search code examples
algorithmagdatheorem-proving

What does errors like "!=<" mean in agda and how to fix


I can't find info about that on http://agda.readthedocs.io/en/v2.5.3/ ,neither on the book "verified programming in agda".What does that mean? And where can I get to know more like this error?

The full error is .cter !=< cter of type Set

The code is sort of missy so if required I would post it later,which is about implementing simulated annealing algorithm .


Solution

  • It literally means that .cter is not a subtype of cter. Since the support for subtyping in Agda is really limited, it most likely means that Agda expected .cter and cter to be equal, but they aren't. In particular, cter is a (visible) variable from your code, while .cter is a hidden argument that Agda introduced and happens to have the same name.

    I hope this helps. It is hard to be more specific without seeing the code, so if you are still stuck please try to find a small example with the same problem and post it here.