Data.Vector3

Stream: mathlib4

[Yaël Dillies]

Could we rename Vector3 to Vector2 or Vector' while we port? We could also backport if you think it matters.

[Henrik Böving]

That's also a thing I've been wondering while porting it, why is it called Vector3 in the first place?

[Yaël Dillies]

There used to be a vector2, but it was removed at some point. This all happened before I started using Lean.

[Chris Hughes]

I've just reviewed it and the only issue I would have before merging is that the notations declared at the top are still global. I haven't worked out how to use scoped in Lean4 yet and I don't think it works with the notation3 command.

[Eric Wieser]

Let's just backport? Or has someone already started porting it?

[Chris Hughes]

It's already basically ported. mathlib4#1204

[Mario Carneiro]

Let's not rename the file unless the change is backported

[Ruben Van de Velde]

Can't we replace it by Vector in the single file that uses it, if we're gonna mess with it?

[Mario Carneiro]

I think the name Vector is likely to be reappropriated for something else anyway

[Mario Carneiro]

For now let's just copy things over, we can refactor later

[Eric Wieser]

I've just pushed some meta code to this PR that adds the [x, y, z] notation promised in the module docstring

[Eric Wieser]

Could someone familiar with this type of thing take a look?

[Matthew Ballard]

I know little about these things but Mario’s alternate suggestion seems to work nicely. Is there anything else holding this up?

[Eric Wieser]

Someone just needs to commit Mario's suggestion

[Mario Carneiro]

did I make a suggestion in this thread?

[Matthew Ballard]

On the PR