[Agda] Re: Vec _ n cong by n

[Francesco Mazzoli]

At Wed, 19 Jun 2013 20:16:48 +0400,
Sergei Meshveliani 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.
> 

‘cong’ is to get a new equality proof by applying a function on both
sides of an existing equality.

What you need here is something that substitutes equal with equal (in
this case ‘length xs’ with ‘n’) in some type type (in this case ‘Vec \bn
(length xs)’), which is precisely what ‘subst’ does.

Francesco