[Agda] Instance arguments vs auto in Idris.

[Apostolis Xekoukoulotakis]

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.

 I am mostly referring to the lhs variables.

What you propose is a nice hack that is only useful if the constructed
proof is proportionally bigger.

On Tue, Oct 31, 2017 at 8:01 PM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171031/6c438f97/attachment.html>