Implicitness juggling

Stream: general

[Yaël Dillies]

I have a (not so) long list of instances (k : Type*) [ordered_ring k] [module k E] and for some isolated lemmas I instead want to use {k : Type*} [ordered_ring k] [module k E] . Is there a way to change the implicitness of k without having to redeclare the instances every time?

[Anne Baanen]

variables {k}?

[Yakov Pechersky]

variables {k} somewhere after you declared it originally

[Yakov Pechersky]

And then similarly, (k) when you want to make it explicit again

[Yaël Dillies]

I know about that, but I also heard someone (Eric?) saying it wasn't actually changing the implicitness of the variable but instead declaring a new one. Is that bad?

[Anne Baanen]

I use variables {k} successfully a lot, so you might be confusing it with something else?

[Yakov Pechersky]

It can't be declaring a new one because then the identifiers would clash.

[Yaël Dillies]

Okay great :smile:

[Yakov Pechersky]

But of course, if you're doing it not in a "variables" command but actually inline after "def" or "lemma", then yes, it declares a brand new variable, just for the scope of the definition/lemma