[Agda] Vec _ n cong by n
Jesper at sikanda.be
Wed Jun 19 19:28:12 CEST 2013
By pattern matching on the proof |xs|=n:
f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n
f xs .(length xs) refl = fromList xs
Also, you don't need to use a where clause in this case.
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
> 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,
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda