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