Mathlib.Vector

Stream: new members

[Burkhardt Renz]

Hi,
how can I define a Vector Nat n literally?

I tried

def v1 : Vector Nat 3 := ([1, 2, 3], rfl)

but got
type mismatch ([1, 2, 3], ?m.252) has type List ?m.235 × ?m.194 : Type (max ?u.234 ?u.191) but is expected to have type Vector ℕ 3 : Type

Are there some examples of using Vector on GitHub?

[Shreyas Srinivas]

@loogle Vector.fromList

[loogle]

:exclamation: unknown identifier 'Vector.fromList'
Did you mean "Vector.fromList"?

[Shreyas Srinivas]

Oh wait this is mathlib vectors. Those are just subtypes with a list and a size proof

[Shreyas Srinivas]

I will send an example in a min

[Shreyas Srinivas]

import Mathlib

def ex1 : Mathlib.Vector ℕ 3 := ⟨[1,2,3], by simp[List.length]⟩

[Shreyas Srinivas]

the mistake in your example is that you are using brackets which are meant for tuples

[Shreyas Srinivas]

What you need are constructor brackets ⟨...⟩

[Burkhardt Renz]

Okay thanks!

How to type the constructor brackets in Visual Studio Code?

[Shreyas Srinivas]

\<...\>. In general you can copy paste unicode notation in your editor and hover over it to get the ascii shortcut for printing these characters

[Burkhardt Renz]

thanks!