vector type

Stream: new members

[Jalex Stark]

Brandon Brown said:

Hoping someone help me understand the vector α n type . It's supposed to be a kind of list of type α of length n but I don't see how this type enforces the length to be n

inductive vector (α : Type u) : nat → Type u
| nil {}                              : vector zero
| cons {n : ℕ} (a : α) (v : vector n) : vector (succ n)

I'm not really sure how to use this type.

it enforces the length to b n by induction. You can see an n on the LHS and a succ n on the RHS

[Jalex Stark]

what do you want to do with vector?

[Brandon Brown]

So if I do vector.cons ℕ vector.nil that creates a type within the vector type family?

[Brandon Brown]

I'm still wrapping my head around the inductive family thing

[Jalex Stark]

vector 3 is a type

[Brandon Brown]

How do I create a vector of natural numbers of length e.g. 2?

[Jalex Stark]

def v : vector ℤ 3 := vector.cons (-1 : ℤ) (vector.cons (0) (vector.cons 0 vector.nil))
#print v

[Jalex Stark]

the notation that comes out of the print is also a valid thing to put in

[Brandon Brown]

Hm ok so that created the type, now how do I add elements to it?
like for list you just keep doing list.cons h (list.cons h (list.nil))) or whatever

[Brandon Brown]

But in this case its supposed to limit it to length 3

[Brandon Brown]

Oh you already added elements - oh man I'm really confused

[Brandon Brown]

Ohh I get it now - thanks