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'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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>