Floris van Doorn

You insert an extra underscore there? I didn't know that. Did you discuss on Zulip to add this to the style? Seems reasonable to me, but it is also pretty...

please mark as `awaiting-review` if it's ready for review

There are two (fixable) issues: * `setup_tactic_parser` opens namespaces, which `open_locale` currently cannot do. This is easily fixed. * It would require a bunch more tactic files to import `tactic.localized`...

It's like 50 lines, excluding the header of the file. It depends on the function `emit_code_here`, but nothing else. I could see some use cases for `open_locale` opening namespaces. For...

Yes, it it worth checking out what was done in the Lean 2 HoTT library (also e.g. https://github.com/leanprover/lean2/blob/master/hott/homotopy/chain_complex.hlean). What I would do the same: * Have the concept of a...

Thanks! bors merge bors d+

Thanks! bors merge

Can we add deprecated aliases for the old names? Maybe only some of the main lemmas?

Other than that, I'm very much in favor of this, but the poll is indeed not as one-sided as I would have hoped.

Thanks! I'm happy to merge it now. @eric-wieser do you think the full rename list is important if we have deprecated the old names?