<br><div class="gmail_quote">On Fri, May 11, 2012 at 7:36 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">
hello,<br>
<br>
I have a problem using "with". The code below is a simplified 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></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'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'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>> 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 | f2 n<br>> ... | no ¬p | _ = f1 n<br>> ... | yes p | f2n = f2n p<br></div>
<div><br></div><div>/ Ulf</div></div>