<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 &lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt; wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
...<br>
Note that &quot;with&quot; 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&#39;m not sure it would have succeeded, the idea was to be able to change the expected argument type of &quot;swap&quot; so that I could easily change the type of its given argument &quot;xs&quot; in an expression containing &quot;swap xs&quot;<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>
&lt;<a href="mailto:cjenkin1@trinity.edu" target="_blank">cjenkin1@trinity.edu</a> &lt;mailto:<a href="mailto:cjenkin1@trinity.edu" target="_blank">cjenkin1@trinity.edu</a>&gt;&gt; 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  &lt;&gt;&lt;      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>