[Agda] signature for `with' branch

[Wolfram Kahl]

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