Kevin Buzzard (Jan 28 2020 at 14:17):
I'm away from a computer right now so am browsing PRs on my phone. I just saw an
open_locale matrix. I've only ever opened
classical. Where can I read about what other locales can be opened?
Bryan Gin-ge Chen (Jan 28 2020 at 15:14):
I don't think there's a list in the docs (yet), but when you get back to a computer you can put the following in a file to get a list of all imported locales:
run_cmd do m ← localized_attr.get_cache, tactic.trace m.keys -- change to `tactic.trace m.to_list` -- to list all the commands in each namespace
I put this in #1874, but that's currently stalled since I haven't been able to reproduce how the current mathlib docs are created.
Yury G. Kudryashov (Jan 28 2020 at 15:56):
You can also grep sources for the word localized
Floris van Doorn (Jan 28 2020 at 17:42):
You can also see which commands are executed when writing
open_locale matrix by executing
run_cmd print_localized_commands [`matrix]
Last updated: May 13 2021 at 06:15 UTC