You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, many old files (in topology and elsewhere) still use Greek letters for topological spaces.
Newer files use e.g. the letters X, Y and Z. We should switch to using these everywhere (per Zulip discussion.
A lot of files have already been converted, but there is still a fair number to go.
Which files are affected? As an approximation, search for files containing the string TopologicalSpace α. As of January 20th, 2024, there are 95 such files in Topology alone (of which 3 have open PRs), and 145 files in all of mathlib.
VS Code's rename handler is useful for renaming variables: go to the declaration site (e.g. a variable statement mentioning something like {α : Type*} or {α : Type u}, select the variable name and press F2.
Sometimes, that doesn't catch all occurrences and you need to rename again. You'll also need to check if docstrings mention α.
The text was updated successfully, but these errors were encountered:
Currently, many old files (in topology and elsewhere) still use Greek letters for topological spaces.
Newer files use e.g. the letters X, Y and Z. We should switch to using these everywhere (per Zulip discussion.
A lot of files have already been converted, but there is still a fair number to go.
Which files are affected? As an approximation, search for files containing the string
TopologicalSpace α
. As of January 20th, 2024, there are 95 such files inTopology
alone (of which 3 have open PRs), and 145 files in all of mathlib.How to replace? What to look out for?
variable
statement mentioning something like{α : Type*}
or{α : Type u}
, select the variable name and press F2.Sometimes, that doesn't catch all occurrences and you need to rename again. You'll also need to check if docstrings mention α.
The text was updated successfully, but these errors were encountered: