<div dir="ltr"><div><div>Instance search does check solutions for *definitional* equality. The problem in your case is that `q` is only propositionally (provably) equal to `z≤n`. I think it's a bit too much to ask of instance search that it would look for proofs that two candidate solutions are equal.<br><br></div>Did you have a particular suggestion for what kind of smartness improvement would make this work?<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div><div><div>Currently, instance resolution tries all possible ways to construct an instance argument.<br><br></div>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.<br><br></div>example :</div><div><br></div><div> Assuming we have defined "less than" as instance.<br><br></div>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.<br></div><br></div>But q is  in fact z≤n.<br><br><br></div>We can prove that there is only one possible construction of the type, thus any variables with the same type are the same.<br></div><div><br></div><div>At the moment, I am trying to prune my context but it would be nice if instance resolution was a bit smarter.<br></div></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>