[Agda] Vec _ n cong by n
mechvel at botik.ru
Thu Jun 20 10:43:01 CEST 2013
On Wed, 2013-06-19 at 20:16 +0200, Jesper Cockx wrote:
> 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.
I thank you and Francesco for helpful remarks.
I knew the meaning of dotted patterns, but decided to avoid them --
while possible, and see further. I have forgotten of them, and now was
not able to use them in this concrete example.
Further, I have a feeling that something is strange in the Language.
Suppose that a type
depends on a : C, A : Setoid, C = Carrier A,
the equivalence p : a \~~ b is proved,
f : Foo a is built,
and we need to return f : Foo b,
and also somehow to express that f : Foo a can be replaced with
f : Foo b if a \~~ b.
Can this be expressed in Agda ?
> > 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
More information about the Agda