<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="im HOEnZb">
On 25.11.2014 17:42, Andrea Vezzosi wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On Tue, Nov 25, 2014 at 5:33 PM, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
...<br>
Note that "with" on an expression of function type is rather pointless, as<br>
you can only match on data, not on functions.<br>
</blockquote>
<br>
Sometimes with on an expression is just to have it as a variable in<br>
the context, so that its type or itself can be rewritten by pattern<br>
matching on other stuff.<br></blockquote></span></blockquote><div><br></div><div>This was exactly my intended use case. Even though I'm not sure it would have succeeded, the idea was to be able to change the expected argument type of "swap" so that I could easily change the type of its given argument "xs" in an expression containing "swap xs"<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="im HOEnZb"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
But surely, Agda should make<br>
a more graceful exit in this case.<br>
<br>
On 24.11.2014 01:21, Christopher Jenkins wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
On Sun, Nov 23, 2014 at 4:39 PM, Christopher Jenkins<br>
<<a href="mailto:cjenkin1@trinity.edu" target="_blank">cjenkin1@trinity.edu</a> <mailto:<a href="mailto:cjenkin1@trinity.edu" target="_blank">cjenkin1@trinity.edu</a>>> wrote:<br>
<br>
However, this is *not* that situation here. Agda has mysteriously<br>
eaten n : Nat, and replaced its occurrences with *a : A* (a<br>
parametric type), generating a type error.<br>
<br>
<br>
Should be: *x : A* (a parametric type)<br>
</blockquote></blockquote></blockquote>
<br>
-- <br></span><div class="HOEnZb"><div class="h5">
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</div></div></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div>Christopher Jenkins<br>Computer Science 2013<br>Trinity University</div></div></div>
</div></div>