[Agda] Instance arguments vs auto in Idris.

[Apostolis Xekoukoulotakis]

http://docs.idris-lang.org/en/latest/tutorial/miscellany.html?#auto-implicit-arguments

On Tue, Oct 31, 2017 at 6:17 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> I am trying to simplify my code by using instance arguments and thus
> letting agda fill them.
>
> I am wondering why Agda does not allow to pick variables that are not
> instance tagged as solutions if there is a unique such solution in the
> context.
>
> A similar feature is the 'auto' in Idris. In this case, auto specifies
> which implicit arguments to automatically fill , with anything found in the
> context.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171031/91e67256/attachment.html>