index of all names

Stream: general

[Johan Commelin]

Do we have a list of all the declarations made in all of mathlib? I couldn't find an index in the docs. The reason this may be useful is in the hypothetical scenario where you have a lot of declarations in a namespace (say gwz) that you want to move to the root namespace. But you need to avoid name conflicts with names from files that you haven't imported. Such an index would be an easy way to figure out that you need to append ''' to mul_div_cancel to make it unique.

[Rob Lewis]

It's not in the docs right now but it's easy enough to generate the list yourself. In a file with import all,

run_cmd do e ← tactic.get_env,
tactic.trace $ list.merge_sort (<) $ e.fold [] $ list.cons ∘ to_string ∘ declaration.to_name

[Mario Carneiro]

You can even filter the list by which names exist in both gwz and _root_ namespace

[Johan Commelin]

Thanks!

[Johan Commelin]

Does it make sense to also add an index to the docs?

[Rob Lewis]

It would be obsolete once there's a better search, no?

[Johan Commelin]

Well, sometimes one might still want to scroll through an alphabetical list... But I agree that it shouldn't be a central feature. (We can also show some stats, like the amount of defs, structures, and thms/lemmas).

[Simon Hudon]

We could put such a list in the zip files being uploaded at the end of each build