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: May 08 2021 at 03:17 UTC