# Zulip Chat Archive

## Stream: new members

### Topic: vec.cons in chapter 2

#### Kritixi Lithos (Dec 07 2019 at 16:47):

Hi, from chapter 2, vec.cons is defined as `constant cons : Π {α : Type u} {n : ℕ}, α → vec α n → vec α (n + 1)`

(I made the args optional). Trying `#check cons 5`

works as expected, but doing `#check cons 5 (vec nat 10)`

gives an error

error: type mismatch at application cons 5 (vec ℕ 10) term vec ℕ 10 has type Type : Type 1 but is expected to have type vec ?m_1 ?m_2 : Type ?

What is it that I am doing wrong?

#### Marc Huisinga (Dec 07 2019 at 17:01):

the definition of `cons`

should be read as follows: given a value of type `α`

and a value of type `vec α n`

, you get a value of type `vec α (n + 1)`

. you are passing `vec nat 10`

, which is a type itself, not a value of type `vec α n`

(similar to how ℕ is a type while 5 is a value of type ℕ).

an example that would work is `#check cons 5 empty`

, for instance.

#### Kritixi Lithos (Dec 07 2019 at 17:09):

Thank you, I understand better now. So then to test with my own examples, I'd have to create vectors using these elementary functions

Last updated: Dec 20 2023 at 11:08 UTC