Zulip Chat Archive

Stream: mathlib4

Topic: Vectors/n-tuples


Jesse Slater (Oct 18 2023 at 22:46):

Currently in Mathlib, I have found support for three different kinds of vectors/n-tuples.
Mathlib.Data.Vector
Mathlib.Data.Fin.Tuple.Reflection
Mathlib.Data.Vector3

What is the advantage of choosing one of these over another? Is there one which should be thought of as the default? Are there more that I missed?

Eric Wieser (Oct 18 2023 at 23:28):

I think mathlib pretty much uses Fin n -> A everywhere (i.e. your second import, though Reflection is a weird file to point to)


Last updated: Dec 20 2023 at 11:08 UTC