Zulip Chat Archive

Stream: general

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Zesen Qian (Aug 14 2018 at 19:24):

that is very helpful. Thanks!

view this post on Zulip Simon Hudon (Aug 14 2018 at 19:28):

You're welcome!


Last updated: May 08 2021 at 03:17 UTC