lean4#4814, new variable command

Stream: lean4

[Michael Rothgang]

I'm excited to see lean4#4814, and was wondering the following: currently, the docstring for variables states

currently, you should avoid changing how variables are bound and declare new variables at the same time

Will this still be relevant after this PR? (I was contemplating to write a linter for this --- if this will become obsolete soon, I'll choose a different project. @Sebastian Ullrich

[Kim Morrison]

(I haven't talked to Sebastian about this, but my inclination is that we should keep this advice, as it is at least slightly confusing when both things are happening at once.)

[Sebastian Ullrich]

lean#2789 is independent of my changes, yes

[Michael Rothgang]

Thanks for clarifying. Then I will probably write such a linter in the next few days.