Zulip Chat Archive

Stream: general

Topic: Reordering `variables`

view this post on Zulip 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)?

view this post on Zulip 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