<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<div class="moz-cite-prefix">Le 25/08/2020 à 12:49, András Kovács a
écrit :<br>
</div>
<blockquote type="cite"
cite="mid:CAA3CDBapjT4sJdqFh3omwKaBOY5Mx9ctETNtV4ztTAq+LuBPaA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">Frédéric: by solving only pattern unification
problems, which have definitionaly unique solutions,</div>
</blockquote>
<p>Could you provide a reference please?</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:CAA3CDBapjT4sJdqFh3omwKaBOY5Mx9ctETNtV4ztTAq+LuBPaA@mail.gmail.com">
<div dir="ltr"> 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"
moz-do-not-send="true">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"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
</blockquote>
</body>
</html>