[Agda] signature for `with' branch

[Ulf Norell]

C-c C-h does something in that direction: it gives you the type
of the with function. But you need to get rid of the with first
and put a hole there instead.

/ Ulf

On Tue, Feb 28, 2017 at 3:07 AM, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:

> On Mon, Feb 27, 2017 at 02:11:31PM +0100, Nils Anders Danielsson wrote:
> > If this helps a lot, then I suggest that you do not use with at all. The
> > with expressions are translated into regular Agda code, that you could
> > have written yourself, with some exceptions, one of which is that with
> > applications are not parsed (but they are not needed if you do not use
> > with).
>
> How hard would it be to make that generated code,
> or at least something close to it, visible via an Agsy ``expand-with''
> feature, that, when triggered in an appropriate place,
> turns the closest surrounding ``with'' into a call to an auxiliary function
> and inserts the definition (skeleton) of that auxiliary function?
> (Perhaps even in cases where Agda complains that the with-function
>  has an illegal type, so that one can actually see that with-function
>  and modify its definition until it has a legal type,
>  supported by error messages that are hopefully more understandable
>  than the one about illegal type of with-function...
> )
>
> How desirable would it be to have that functionality?
> I can imagine using it...
>
>
> Wolfram
> _______________________________________________
> 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/20170228/0064c742/attachment.html>