## Stream: Coq users

### Topic: Function to index elements of a vector

#### Julin S (Aug 10 2021 at 13:47):

I was trying to make a way to access elements of a `Vector.t` by the 'index' of the elements (where indexing starts from zero).

I tried:

``````Fixpoint index {A n} (i : nat) (v : Vector.t A n) :
(*match n with*)
match n, v return Type with
| _, nil _        => unit
| _, cons _ _ _ _ => A
end :=
match n, v with
| _, nil _            => tt
| 0, cons _ x _ xs    => x
| S n', cons _ x z xs => index i xs
end.
``````

but am getting error that says:

``````The term "tt" has type "unit" while it is expected to have type
"match ?t@{v:=v0; n2:=0; n3:=0; v1:=[]} with
| [] => unit
| _ :: _ => A
end".
``````

I thought doing the `match` for the return type would've avoided such an error.

How can this be set right?

#### Olivier Laurent (Aug 10 2021 at 19:51):

As far as I understand, you are trying to say that your `index` function returns an element of type `A` whenever `v` is not empty, but your code would give `index (S 0) (cons _ _ _ (nil _)) = tt`.

#### Julin S (Aug 12 2021 at 07:20):

Yeah, I wanted `index` to return an `A` when `v` isn't empty and the index is valid.

I meant indexing to start from 0. `(cons _ _ _ (nil _))` means a vector with a single element, right? So an index of `(S 0)` would be invalid.

I gave `tt` as a way to handle invalid cases (don't even know if that's how it's usually done..).

Edit: Oh.. I see that the index is not taken into account while defining the return type..

Last updated: Oct 03 2023 at 20:01 UTC