vector2

Stream: general

[Eric Wieser]

We have docs#vector and docs#vector3; where's docs#vector2? To make things more confusing, we have data.vector2 which is actually just about vector!

[Patrick Massot]

@Mario Carneiro :up:

[Shing Tak Lam]

I thought data.vector2 is called that because there is a data.vector file in core? (nb. the file in code is data.vector, and not init.data.vector, which is how we have data.nat.basic in mathlib and init.data.nat.basic in core)

[Eric Wieser]

Does lean complain if we rename data.vector2 to data.vector.lemmas?

[Eric Wieser]

ie, is a .lean file allowed to overlap with a directory in a different filesystem?

[Shing Tak Lam]

Yeah that's fine. There's data.dlist in core, and data.dlist.basic and data.dlist.instances in mathlib

[Eric Wieser]

Moved in #8697, but the question about the name of docs#vector3 still applies

[Mario Carneiro]

vector2 existed for a short time in dioph.lean. IIRC, vector is a subtype of list, vector3 is fin n -> A, and vector2 is an inductive family

[Mario Carneiro]

I forget if fin2 n -> A was in there too (since there are two fins, one being the subtype of nat and the other an inductive family)

[Mario Carneiro]

Eric Wieser said:

ie, is a .lean file allowed to overlap with a directory in a different filesystem?

Lean 3 allows arbitrary overlaps here, but if they have the same path it's unpredictable which one you will get, so it is best to avoid that