I'm sorry, I didn't realize you were not familiar with inaccessible (dotted) patterns. There are other ways to define this function (for example by using the rewrite keyword), but dotted patterns are the most basic. Dotted patterns are a really useful technique when writing <i>any</i> program in agda with dependent types, and you shouldn't be afraid of them ;) You can use them whenever the types force a variable into a unique value (not very precise, but a good way to think about it). In this case, pattern matching on |xs|=n forces n to be equal to (length xs), hence the inaccessible pattern. <div>
<br></div><div>Actually, you don't even have to write these patterns by yourself. If you start by writing</div><div><br></div><div>f xs n |xs|=n = ?</div><div><br></div><div>and load the file, you get a 'hole' instead of the question mark. If you place the cursor in that goal and press ctrl-c-c, then enter |xs|=n, agda will write the pattern for you complete with dotted pattern.</div>
<div><br></div><div>I hope this helps,</div><div>Jesper<br>
<br><div class="gmail_quote">On Wed, Jun 19, 2013 at 7:47 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">
<div>On Wed, 2013-06-19 at 19:28 +0200, Jesper Cockx wrote:<br>
> By pattern matching on the proof |xs|=n:<br>
><br>
><br>
> f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n<br>
> f xs .(length xs) refl = fromList xs<br>
</div>> [..]<br>
<br>
This is very new to me!<br>
Really -- no way to implement this without a dotted pattern?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<div><div><br>
<br>
> On Wed, Jun 19, 2013 at 6:16 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>><br>
> wrote:<br>
> 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" target="_blank">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>
><br>
><br>
<br>
<br>
</div></div></blockquote></div><br>
</div>