[Agda] Re: Vec _ n cong by n
f at mazzo.li
Wed Jun 19 18:48:18 CEST 2013
At Wed, 19 Jun 2013 20:16:48 +0400,
Sergei Meshveliani 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.
‘cong’ is to get a new equality proof by applying a function on both
sides of an existing equality.
What you need here is something that substitutes equal with equal (in
this case ‘length xs’ with ‘n’) in some type type (in this case ‘Vec \bn
(length xs)’), which is precisely what ‘subst’ does.
More information about the Agda