Casting List to Vector

Stream: new members

[Benjamin]

How can I cast a term of type List α to type Vector α n?

[Ilmārs Cīrulis]

My approach would be this.

import Mathlib

def ListToVector {α: Type} (L: List α): Vector α L.length :=
  { toList := L, size_toArray := rfl }

[Ilmārs Cīrulis]

(I'm beginner.)

[Ilmārs Cīrulis]

Edited by simp to rfl.

[Eric Wieser]

Alternatively you could use docs#List.Vector

[Benjamin]

Eric Wieser said:

Alternatively you could use docs#List.Vector

Is this a different Vector than Init.Data.Vector?

[Benjamin]

What I'm really trying to do is transpose a vector of vectors (i.e., go from Vector (Vector α n) m to Vector (Vector α m) n). I thought that the easiest way to do this would be to leverage the existing List.transpose function. But that doesn't seem to give me the necessary information to prove that the resulting lists are of the desired lengths. Is there an easier approach?

[Daniel Weber]

I have code for that, let me find it

[Daniel Weber]

https://github.com/leanprover-community/mathlib4/pull/17145/files#diff-cb3184ab826f38d1b4651a62163a407974385054cb52f07687f5630781d573bf

[Matt Diamond]

would it be easier to just use Matrix to represent a vector of vectors? docs#Matrix.transpose already exists