Zulip Chat Archive

Stream: new members

Topic: vec.cons in chapter 2


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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: May 14 2021 at 02:15 UTC