<br><div class="gmail_quote">On Fri, May 11, 2012 at 9:52 PM, Guillermo Calderón <span dir="ltr"><<a href="mailto:calderon@fing.edu.uy" target="_blank">calderon@fing.edu.uy</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 11/05/12 16:24, Ulf Norell wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
<br>
On Fri, May 11, 2012 at 7:36 PM, Guillermo Calderón<br>
<<a href="mailto:calderon@fing.edu.uy" target="_blank">calderon@fing.edu.uy</a><br></div><div class="im">
<mailto:<a href="mailto:calderon@fing.edu.uy" target="_blank">calderon@fing.edu.uy</a>>> wrote:<br>
<br>
  hello,<br>
<br>
  I have a problem using "with".  The  code below  is a simplified<br>
  version to illustrate the case:<br>
<br>
  > g :  ℕ  → ℕ<br>
  > g a with  a ≤? 5<br>
  > ... |  yes _  = a<br>
  > ... |  no  _  = suc a<br>
  ><br>
  > prop-g  : ∀ n  -> (R :  ℕ  → Set)<br>
  >         -> (∀ m -> R (suc m))<br>
  >         -> (∀ n -> n ≤ 5 -> R (g n))<br>
  >         -> R (g n)<br>
  > prop-g n R f1 f2  with n ≤? 5<br>
  > ... | no  ¬p  =  f1 n<br>
  > ... | yes p   =  f2 n p- -*** ERROR here ***<br>
  ><br>
<br>
<br>
The problem is that the abstraction happens at the point of the<br>
with. At that point you haven't applied f2 yet, so the n in the type<br>
of f2 is a different n from the one in n ≤? 5, thus it doesn't abstract.<br>
<br>
</div></blockquote>
<br>
Ulf,<br>
Thanks for your answer.<br>
As far as i known, the same problem should happen for the case (no  ¬p).<div class="im"><br>
<br>
   > ... | no  ¬p  =  f1 n<br>
<br></div>
However,  no error is reported by agda at this level and  (f1 n)  is accepted as well typed.<br>
¿what is the difference between  both cases?</blockquote><div><br></div><div>In the no case you don't need the g n in f2 to reduce. The g n in the goal gets abstracted over</div><div>without problems when you do the with.</div>
<div><br></div><div>/ Ulf </div></div>