<div dir="ltr"><div><div><div>lpaste here: <a href="http://lpaste.net/114815">http://lpaste.net/114815</a><br><br></div>I am aware that a function generated by "with" is not always well-typed. I'm to understand this is limited to cases where, for example, function foo takes as its argument B (bar a), where a : A and B : A -> Set, and we have rewritten "bar a" to some "w", but foo remains untouched (i.e. its external to the context).<br><br></div>However, this is <b>not</b> that situation here. Agda has mysteriously eaten n : Nat, and replaced its occurrences with a : A (a parametric type), generating a type error. I can't imagine this is anything other than a bug, but if it isn't I'd at least like to know the rationale behind this behaviour.<br><br></div>Note that I am aware that this definition of "swap" is terrible. I was playing with Agda to see if I could push it to see the function is involutive even in such a situation when I encountered this.<br><div><br>Thanks.<br clear="all"><div><div><div><div><br>-- <br><div class="gmail_signature"><div dir="ltr"><div>Christopher Jenkins<br>Computer Science 2013<br>Trinity University</div></div></div>
</div></div></div></div></div></div>