[Agda] Vec _ n cong by n

[Sergei Meshveliani]

On Wed, 2013-06-19 at 19:28 +0200, Jesper Cockx wrote:
> By pattern matching on the proof |xs|=n:
> 
> 
> f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n
> f xs .(length xs) refl = fromList xs
> [..]

This is very new to me!
Really -- no way to implement this without a dotted pattern? 

Thanks,

------
Sergei


> 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
> 
>