why [variable_alias] attribute is not used in Mathlib?

Stream: mathlib4

[Asei Inoue]

why [variable_alias] attribute is not used in Mathlib?
[variable_alias] attribute seems to appear only in output of #help command.

[Asei Inoue]

https://seasawher.github.io/mathlib4-help/attributes/#variable_alias

[Kim Morrison]

Because we never started using it!

[Kim Morrison]

It remains tempting.

[Asei Inoue]

Because we never started using it!

Why is it not being used? Are there any plans to use it?

[Jireh Loreaux]

oh, I think @Pieter Cuijpers might really appreciate this for quantales, especially for the mixin route.

[Kim Morrison]

Asei Inoue said:

Because we never started using it!

Why is it not being used? Are there any plans to use it?

As I said above, because no one made a PR. (This is the reason for most questions beginning "Why isn't..." about Mathlib!)

[Eric Wieser]

Well, sometimes it's "because someone did make a PR and it caused trouble", but that doesn't apply here

[Pieter Cuijpers]

Indeed, I would love that!
But I sadly lack the expertise to work on a PR for it...

[Jireh Loreaux]

I don't think you understand. You can use it now.

[Pieter Cuijpers]

Oh great :-)

[Asei Inoue]

I would like to submit a PR too, but I don't think I am the right person for it.

[Kim Morrison]

Asei Inoue said:

I would like to submit a PR too, but I don't think I am the right person for it.

What is the obstacle?

[Asei Inoue]

What is the obstacle?

I have no time & knowledge

[Julian Berman]

I figured I'd PR literally the trivial example from variable_alias (i.e. VectorSpace) given how often it's asked about (#19212). But when I tried to add an example of how to use it to the file, I couldn't think of a RHS that didn't look alien. Specifically:

/-- If 𝔽 is a field, 𝔽^n is a vector space over 𝔽. -/
example {𝔽 : Type*} [Field 𝔽] {n : ℕ} : VectorSpace 𝔽 (Fin n → 𝔽) := {}

I got that {} from exact?, and I guess I follow what it means, it's saying "all the data for a vector space is already inferred from the typeclass system finding those 3 other type classes" -- but it .. looks weird doesn't it? I tried putting infer_instance there instead, and Lean tells me vector space indeed isn't a class (which I guess the docs for variable_alias also tell me). I'm re-reading the docs as I'd only skimmed them before, but is there something obviously clearer to put there?

[Julian Berman]

I guess what I wanted to write (reading slightly more carefully) is to call into however variable? itself works to get a RHS.

[Julian Berman]

I suppose another question is whether any extra lemmas are needed when defining an alias. Regardless maybe putting up the trivial PR is a good way to get someone to spit out some ideas.