<div dir="ltr">C-c C-h does something in that direction: it gives you the type<div>of the with function. But you need to get rid of the with first</div><div>and put a hole there instead.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 28, 2017 at 3:07 AM, Wolfram Kahl <span dir="ltr"><<a href="mailto:kahl@cas.mcmaster.ca" target="_blank">kahl@cas.mcmaster.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Mon, Feb 27, 2017 at 02:11:31PM +0100, Nils Anders Danielsson wrote:<br>
> If this helps a lot, then I suggest that you do not use with at all. The<br>
> with expressions are translated into regular Agda code, that you could<br>
> have written yourself, with some exceptions, one of which is that with<br>
> applications are not parsed (but they are not needed if you do not use<br>
> with).<br>
<br>
</span>How hard would it be to make that generated code,<br>
or at least something close to it, visible via an Agsy ``expand-with''<br>
feature, that, when triggered in an appropriate place,<br>
turns the closest surrounding ``with'' into a call to an auxiliary function<br>
and inserts the definition (skeleton) of that auxiliary function?<br>
(Perhaps even in cases where Agda complains that the with-function<br>
 has an illegal type, so that one can actually see that with-function<br>
 and modify its definition until it has a legal type,<br>
 supported by error messages that are hopefully more understandable<br>
 than the one about illegal type of with-function...<br>
)<br>
<br>
How desirable would it be to have that functionality?<br>
I can imagine using it...<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
Wolfram<br>
</font></span><div class="HOEnZb"><div class="h5">______________________________<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>
</div></div></blockquote></div><br></div>