[Agda] Vec _ n cong by n

[Jesper Cockx]

By pattern matching on the proof |xs|=n:

f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n
f xs .(length xs) refl = fromList xs

Also, you don't need to use a where clause in this case.


Jesper

On Wed, Jun 19, 2013 at 6:16 PM, Sergei Meshveliani <mechvel at botik.ru>wrote:

> Please, how to fix the following code?
>
>   f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n
>   f xs n |xs|=n =  v
>                    where
>                    v : Vec ℕ (length xs)
>                    v = fromList xs
>
> The type of  v  does not match.
>
> According to  |xs|=n,  length xs  can be replaced with  n  in
> Vec ℕ (length xs).
> But probably,  cong  is not for  Vec  ...
> So I wonder.
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130619/3769b5a8/attachment.html