[Agda] Hanging out with the Lean crowd

[András Kovács]

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.

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.

Frédéric Blanqui <frederic.blanqui at inria.fr> ezt írta (időpont: 2020. aug.
25., K, 12:33):

> Hi. How do you know that a unification problem in Agda (hence modulo
> definitional equality right?) has a unique solution?
>
> Le 25/08/2020 à 10:56, Nils Anders Danielsson a écrit :
> > On 2020-08-25 06:42, Henning Basold wrote:
> >> reasoning about commuting diagrams in category theory is quite neat to
> >> do in Agda, although better heuristics to figure out implicit
> >> arguments need to be implemented.
> >
> > Unlike several other systems Agda does not instantiate implicit
> > arguments unless the solution is unique (if we ignore bugs). Do you have
> > an example where Agda fails to find a unique solution, and you think
> > Agda should have found it? In that case, please post it on the bug
> > tracker.
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200825/13373ee8/attachment.html>