'variable' - style question

Stream: mathlib4

[Michael Stoll]

In a comment on #11214, @Chris Birkbeck suggested to factor out some of the repeatedly used arguments into a variable declaration. I'm inclined to not do that (there are not many arguments, and they are explicit in some declarations and implicit in others), but I would like to know if there are some agreed-upon style guidelines on when to use variables and when not to. I think one point (also from a comment on a recent PR) is:

• Do not put assumptions (arguments whose type is a Prop) in a variabledeclaration.
  (Rationale: the statement is obfuscated if the assumptions are not visible).

Are there more considerations one should keep in mind?

[Yaël Dillies]

Do you know that you can do variable (assumption)/variable {assumption} to change implicitness of an argument?

[Michael Stoll]

Yes. But having to switch between explicit and implicit repeatedly defeats the purpose of the variable declaration to some extent.

[Chris Birkbeck]

Sorry maybe I wasn't clear, I just meant use it in all the places you have it implicit, since it was showing up in several places and just leave it in the explicit ones. But it was just a thought, I don't really have strong feelings either way.

[Michael Stoll]

In the concrete case, I think that the trade-off is pointing fairly clearly toward not using variable. It would not make the file shorter (the arguments fit on the same line as the lemma name), but a bit harder to read (in particular if f, s etc. are mentioned sometimes (when explict) and sometimes not).

This will look different when one can avoid having to list half a dozen typeclass arguments each time.

[Damiano Testa]

Also, try to use variable only in a situation where the variables really should be part of the signature of the declaration: unless you are careful, lean may use some "unused" ones.