vec.cons in chapter 2

Stream: new members

[Kritixi Lithos]

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]

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]

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