open classical

Stream: mathlib4

[Yury G. Kudryashov]

Is it possible to add instances but not definitions from Classical to the scope?

[Yury G. Kudryashov]

If I open Classical, then I have to use _root_. or Classical. here and there.

[Yaël Dillies]

I guess it's just a matter of protecting them?

[Yury G. Kudryashov]

Or dropping some of our lemmas in the root NS and replacing them with export Classical (not_not) etc.

[Eric Rodriguez]

having to have this workaround seems annoying. i wonder if there's a need for a separate sort of open

[Mario Carneiro]

Yury G. Kudryashov said:

Is it possible to add instances but not definitions from Classical to the scope?

yes, open scoped Classical opens scoped instances/notation but not names, roughly equivalent to open Classical hiding (*)

[Gabriel Ebner]

Is there anything besides not_not that is causing issues? Because we definitely shouldn't have duplicate not_not and unprotected Classical.not_not lemmas. We avoid that everywhere else and so we should here.

[Yury G. Kudryashov]

I'll make another PR if I see anything else. Maybe, we have by_contra or by_cases in both root and Classical.