Implicit variables like v✝

Stream: lean4

[Bjørn Kjos-Hanssen]

In Lean 4 implicit variables seem to be appear more frequently in the Infoview than I recall from Lean 3.
Often, I want to close the goal using v✝, but it is not allowed (error: "expected token").
What's the general methodology to make variables explicit? Concretely, "how do I turn v✝ into v?"

[Kyle Miller]

These variables are known as "inaccessible", and they generally arise when Lean generates the name itself.

There are a number of ways to make inaccessible variables be accessible. Some ways are via knowing variants of a tactic (for example, induction and cases let you name variables using a pattern-matching-like syntax). Others are by using extra tactics that are just for renaming, like rename_i ("rename inaccessibles").

[Kyle Miller]

I like the next u v w => ... tactic for doing rename_i while simultaneously focusing on the first goal.

[Bjørn Kjos-Hanssen]

rename_i seems quite :tada: here.

[Scott Morrison]

That said, rename_i is a bit ugly. It's better to use structured tactics that result in the hypotheses having accessible names from the beginning.

[Kevin Buzzard]

Yeah, the right question isn't "how do I access this variable whose name has a dagger", it's "how did this variable get a name with a dagger in the first place and what should I have done instead"

[Eric Rodriguez]

I think sometimes it'd be useful to access daggered variables. I wouldn't mind it if it was put behind a set_option.

[Alex J. Best]

Eric Rodriguez said:

I think sometimes it'd be useful to access daggered variables. I wouldn't mind it if it was put behind a set_option.

That's set_option tactic.hygienic false

[Bjørn Kjos-Hanssen]

Alex J. Best said:

Eric Rodriguez said:

I think sometimes it'd be useful to access daggered variables. I wouldn't mind it if it was put behind a set_option.

That's set_option tactic.hygienic false

Great, that'll do as a crutch. One can work on getting by without it in due time.