2018-01-11 09:03:27 UTC
It will look for arguments in the environment and it will use instance
functions to create new ones. If there are multiple solutions, instance
resolution will fail.
Assuming we have defined "less than" as instance.
if we have in the context, a variable q with type zero â€ (suc zero) ,
instance resolution will fail because there are two solutions, q and zâ€n.
But q is in fact zâ€n.
We can prove that there is only one possible construction of the type, thus
any variables with the same type are the same.
At the moment, I am trying to prune my context but it would be nice if
instance resolution was a bit smarter.