<div dir="ltr">Frédéric: by solving only pattern unification problems, which have definitionaly unique solutions, and reducing every non-pattern problem to pattern problems by various strategies, e.g. by constraint postponing or eta conversion.<div><br></div><div>However, this uniqueness is only about unification, but that's just one part of elaboration. There is also a degree of freedom in deciding where to insert implicit applications and lambdas, and Agda's choice of insertions is not really unique. In general, I think it's practically realistic to have unification which produces unique solutions, but not that realistic to have elaboration which produces unique output. </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Frédéric Blanqui <<a href="mailto:frederic.blanqui@inria.fr" target="_blank">frederic.blanqui@inria.fr</a>> ezt írta (időpont: 2020. aug. 25., K, 12:33):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi. How do you know that a unification problem in Agda (hence modulo <br>
definitional equality right?) has a unique solution?<br>
<br>
Le 25/08/2020 à 10:56, Nils Anders Danielsson a écrit :<br>
> On 2020-08-25 06:42, Henning Basold wrote:<br>
>> reasoning about commuting diagrams in category theory is quite neat to<br>
>> do in Agda, although better heuristics to figure out implicit<br>
>> arguments need to be implemented.<br>
><br>
> Unlike several other systems Agda does not instantiate implicit<br>
> arguments unless the solution is unique (if we ignore bugs). Do you have<br>
> an example where Agda fails to find a unique solution, and you think<br>
> Agda should have found it? In that case, please post it on the bug<br>
> tracker.<br>
><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>