<br><div class="gmail_quote">On Fri, May 11, 2012 at 7:36 PM, Guillermo Calderón <span dir="ltr">&lt;<a href="mailto:calderon@fing.edu.uy" target="_blank">calderon@fing.edu.uy</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

hello,<br>
<br>
I have a problem using  &quot;with&quot;.  The  code below  is a simplified version to illustrate the case:<br>

<br>
&gt; g :  ℕ  → ℕ<br>
&gt; g a with  a ≤? 5<br>
&gt; ... |  yes _  = a<br>
&gt; ... |  no  _  = suc a<br>
&gt;<br>
&gt; prop-g  : ∀ n  -&gt; (R :  ℕ  → Set)<br>
&gt;                -&gt; (∀ m -&gt; R (suc m))<br>
&gt;                -&gt; (∀ n -&gt; n ≤ 5 -&gt; R (g n))<br>
&gt;                -&gt; R (g n)<br>
&gt; prop-g n R f1 f2  with n ≤? 5<br>
&gt; ... | no  ¬p   =  f1 n<br>
&gt; ... | yes p    =  f2 n p- -*** ERROR here ***<br>
&gt;<br></blockquote><div><br></div><div>The problem is that the abstraction happens at the point of the</div><div>with. At that point you haven&#39;t applied f2 yet, so the n in the type</div><div>of f2 is a different n from the one in n ≤? 5, thus it doesn&#39;t abstract.</div>

<div><br></div><div>One solution is to also abstract over the application of f2. Untested</div><div>code:</div><div><br></div><div>&gt; prop-g  : ∀ n  -&gt; (R :  ℕ  → Set)<br>&gt;                -&gt; (∀ m -&gt; R (suc m))<br>

&gt;                -&gt; (∀ n -&gt; n ≤ 5 -&gt; R (g n))<br>&gt;                -&gt; R (g n)<br>&gt; prop-g n R f1 f2  with n ≤? 5 | f2 n<br>&gt; ... | no  ¬p   | _   =  f1 n<br>&gt; ... | yes p    | f2n =  f2n p<br></div>

<div><br></div><div>/ Ulf</div></div>