[Agda] Vec _ n cong by n
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