By pattern matching on the proof |xs|=n:<div><br></div><div>f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n</div><div>f xs .(length xs) refl = fromList xs</div><div><br></div><div>Also, you don&#39;t need to use a where clause in this case.</div>

<div><br></div><div><br></div><div>Jesper<br><br><div class="gmail_quote">On Wed, Jun 19, 2013 at 6:16 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Please, how to fix the following code?<br>
<br>
  f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n<br>
  f xs n |xs|=n =  v<br>
                   where<br>
                   v : Vec ℕ (length xs)<br>
                   v = fromList xs<br>
<br>
The type of  v  does not match.<br>
<br>
According to  |xs|=n,  length xs  can be replaced with  n  in<br>
Vec ℕ (length xs).<br>
But probably,  cong  is not for  Vec  ...<br>
So I wonder.<br>
<br>
Thank you in advance for explanation,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>