[Agda] Hanging out with the Lean crowd

[Nils Anders Danielsson]

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.

-- 
/NAD