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):
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
Zesen Qian (Aug 14 2018 at 19:24):
that is very helpful. Thanks!
Simon Hudon (Aug 14 2018 at 19:28):
Last updated: May 08 2021 at 03:17 UTC