(meta) get a list of all definition in a file

Stream: general

[Zesen Qian]

Hi, is it possible in meta-programming to get a list of all (non-meta) definitions in a file?

[Simon Hudon]

Yes. There are three parts to this: listing (or folding over) the visible definitions, determining that they are from the current file and determining whether they are definitions.

[Zesen Qian]

I guess the hard part is the first then. I browsed thorough tactic.lean and didn't find anything interesting.

[Simon Hudon]

In init.meta.environment, you can find environment.fold. It doesn't give you a list but it lets you iterate over all the definitions of a file and accumulate them. get_env gives you the current environment and in_current_file' tells you if a given name is defined / declared in the current file and finally, you can look at the declaration data structure and see the trusted bit for definition and constant.

[Zesen Qian]

that is very helpful. Thanks!

[Simon Hudon]

You're welcome!