# Zulip Chat Archive

## Stream: general

### Topic: Reordering `variables`

#### Eric Wieser (Oct 15 2020 at 09:10):

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 (Oct 15 2020 at 19:21):

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...

Last updated: Aug 03 2023 at 10:10 UTC