[Agda] problem using "with"
Guillermo Calderón
calderon at fing.edu.uy
Fri May 11 19:36:42 CEST 2012
hello,
I have a problem using "with". The code below is a simplified
version to illustrate the case:
> g : ℕ → ℕ
> g a with a ≤? 5
> ... | yes _ = a
> ... | no _ = suc a
>
> prop-g : ∀ n -> (R : ℕ → Set)
> -> (∀ m -> R (suc m))
> -> (∀ n -> n ≤ 5 -> R (g n))
> -> R (g n)
> prop-g n R f1 f2 with n ≤? 5
> ... | no ¬p = f1 n
> ... | yes p = f2 n p- -*** ERROR here ***
>
_≤?_ is the decidable total order relation from the standard library
Data.Nat
Agda gives this error message:
> g n | n ≤? 5 != n of type ℕ
> when checking that the expression f2 n p has type R (g n | yes p)
However (g n) reduces to n for the case | yes p.
What's wrong with the above?
Thanks for your help.
Guillermo
More information about the Agda
mailing list