[Agda] Instance arguments vs auto in Idris.

[Apostolis Xekoukoulotakis]

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/3cfdf3d1/attachment.html>