<div dir="ltr"><div><div>I haven't used Idris for a while but in the documentation, it says that using something in the outer context requires the "%hint" annotation, so this is similar to how we need to annotate functions with instance in Agda.<br><br></div> I am mostly referring to the lhs variables.<br><br></div>What you propose is a nice hack that is only useful if the constructed proof is proportionally bigger.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 31, 2017 at 8:01 PM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">By "in the context", you only mean things bound by let and on<br>
left-hand sides, right? Not everything in scope? Allowing everything<br>
in scope would make instance search prohibitively slow when using big<br>
libraries.<br>
<br>
If you do mean variables bound on left-hand sides, I’m not quite sure<br>
either why explicit arguments are not available for instance search<br>
but note that<br>
- instance arguments *are* available for instance search, as you<br>
mention, so even though in<br>
<br>
f : A -> B<br>
f a = ?<br>
<br>
the [a] is not available for instance search in the goal, it is available in<br>
<br>
f : {{_ : A}} -> B<br>
f = ?<br>
<br>
- In case you need explicit arguments to be available for instance<br>
search, you can use the following workaround:<br>
<br>
f : A -> B -> C<br>
f a b = ? where instance _ = a; _ = b<br>
<br>
Now both [a] and [b] are available for instance search.<br>
<br>
On Tue, Oct 31, 2017 at 12:47 PM, Apostolis Xekoukoulotakis<br>
<span class=""><<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@<wbr>gmail.com</a>> wrote:<br>
> <a href="http://docs.idris-lang.org/en/latest/tutorial/miscellany.html?#auto-implicit-arguments" rel="noreferrer" target="_blank">http://docs.idris-lang.org/en/<wbr>latest/tutorial/miscellany.<wbr>html?#auto-implicit-arguments</a><br>
><br>
> On Tue, Oct 31, 2017 at 6:17 PM, Apostolis Xekoukoulotakis<br>
> <<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@<wbr>gmail.com</a>> wrote:<br>
>><br>
>> I am trying to simplify my code by using instance arguments and thus<br>
>> letting agda fill them.<br>
>><br>
>> I am wondering why Agda does not allow to pick variables that are not<br>
>> instance tagged as solutions if there is a unique such solution in the<br>
>> context.<br>
>><br>
>> A similar feature is the 'auto' in Idris. In this case, auto specifies<br>
>> which implicit arguments to automatically fill , with anything found in the<br>
>> context.<br>
><br>
><br>
><br>
</span>> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
</blockquote></div><br></div>