making variables implicit

Stream: mathlib4

[Adam Topaz]

I feel really stupid asking this... is the following supposed to work in lean4?

import Mathlib.CategoryTheory.Functor.Basic

open CategoryTheory
variable (C : Type _) [Category C]

variable {C} (F : C ⥤ C)

[Adam Topaz]

Note that the following is okay:

import Mathlib.CategoryTheory.Functor.Basic

open CategoryTheory
variable (C : Type _) [Category C]

variable {C}
variable (F : C ⥤ C)

[Eric Wieser]

This has come up before, and I think is deliberate

[Eric Wieser]

Changing and adding variables apparently now has to be done in separate variables commands

[Adam Topaz]

okay, fair enough.

[Kevin Buzzard]

You get the impression that they want to make variable deprecated :-) It is terrifying sometimes during porting when some Lean 3 proof is broken and you look at the tactic state and there are a gazillion irrelevant variables in there, just because they were declared 1000 lines earlier and are long forgotten about (they weren't in the corresponding Lean 3 tactic state)

[Adam Topaz]

Personally, I think it would clarify things if the "adding variables" command was called "variable" and the "changing variables" command was called something different.

[Kevin Buzzard]

Now you can't do them both at once, your suggestion makes a lot of sense.

[Mario Carneiro]

Eric Wieser said:

This has come up before, and I think is deliberate

I don't think it is deliberate, it doesn't make much sense from a user perspective

[Sebastian Ullrich]

Yes, this is most likely not deliberate, otherwise it would be a hard error. The problem is that the entire variable binder set is test-elaborated before binders corresponding to binder updates are removed. The fix is not a one-liner from what I can see.

[Adam Topaz]

@Sebastian Ullrich Shall I open an issue in the lean4 repo?

[Sebastian Ullrich]

Yes, please do