[Agda] Hanging out with the Lean crowd

[Neel Krishnaswami]

Hi,

I didn't know that solutions remained unique even if you solved 
constraints lazily. Is there a reference for this?

Best,
Neel

On 25/08/2020 09:56, Nils Anders Danielsson wrote:
>
> 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.
>