[Agda] Instance arguments vs auto in Idris.

[Guillaume Brunerie]

By "in the context", you only mean things bound by let and on
left-hand sides, right? Not everything in scope? Allowing everything
in scope would make instance search prohibitively slow when using big
libraries.

If you do mean variables bound on left-hand sides, I’m not quite sure
either why explicit arguments are not available for instance search
but note that
- instance arguments *are* available for instance search, as you
mention, so even though in

f : A -> B
f a = ?

the [a] is not available for instance search in the goal, it is available in

f : {{_ : A}} -> B
f = ?

- In case you need explicit arguments to be available for instance
search, you can use the following workaround:

f : A -> B -> C
f a b = ? where instance _ = a; _ = b

Now both [a] and [b] are available for instance search.

On Tue, Oct 31, 2017 at 12:47 PM, Apostolis Xekoukoulotakis
<apostolis.xekoukoulotakis at gmail.com> wrote:
> 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.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>