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