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 .
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.