[Agda] Vec _ n cong by n

Sergei Meshveliani mechvel at botik.ru
Wed Jun 19 18:16:48 CEST 2013

Please, how to fix the following code?

  f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n
  f xs n |xs|=n =  v
                   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,


More information about the Agda mailing list