[Agda] Hanging out with the Lean crowd

[Frédéric Blanqui]

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