Reordering `variables`

Stream: general

[Eric Wieser]

If I have some variables in my scope:

variables (a : nat)

and I then much further down the file I declare a lemma with a new variable

lemma foo (f : nat → nat) : f a = 0 := sorry

how can I tell lean to make the signature of foo be (f : nat → nat) (a : nat) : f a = 0 instead of (a : nat) (f : nat → nat) : f a = 0, without having to redeclare a locally (and all of its dependent type classes)?

[Floris van Doorn]

I think that's not possible.
I tend to use variables only/mostly for implicit argument, where the order doesn't matter too much. When needing to make a variable explicit, I like to redeclare them locally (this means it is also easy to see which arguments are explicit, just by looking at the source file.
It seems you have a bunch of typeclasses depending on an explicit variable, which makes this approach not ideal...