[Agda] Vec _ n cong by n

[Jesper Cockx]

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 *any* 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.

Actually, you don't even have to write these patterns by yourself. If you
start by writing

f xs n |xs|=n = ?

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.

I hope this helps,
Jesper

On Wed, Jun 19, 2013 at 7:47 PM, Sergei Meshveliani <mechvel at botik.ru>wrote:

> 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
> >
> >
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130619/0a98529d/attachment.html