Zulip Chat Archive

Stream: general

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


Zesen Qian (Aug 14 2018 at 19:16):

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

Simon Hudon (Aug 14 2018 at 19:18):

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 (Aug 14 2018 at 19:22):

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

Simon Hudon (Aug 14 2018 at 19:23):

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 (Aug 14 2018 at 19:24):

that is very helpful. Thanks!

Simon Hudon (Aug 14 2018 at 19:28):

You're welcome!


Last updated: Dec 20 2023 at 11:08 UTC