Iterate over the environment

Stream: general

[Neil Strickland]

I know essentially nothing about the metaprogramming framework so I am sorry if this question is somehow misconceived.

I would like to write some new commands that summarise information about what Lean knows. My idea was to start with #print prefix and modify it. However, if I understand correctly, #print prefix is implemented by the function print_prefix defined in C++ in the file src/frontends/lean/print_cmd.cpp. That uses a method called for_each_declaration. In Lean I can do some inspection of the environment like this:

meta def foo : tactic unit :=  do env ← tactic.get_env, tactic.trace (environment.contains env `nat)

However, I am not seeing anything in Lean that is equivalent to for_each_declaration. Am I missing something?

Incidentally, tactic_writing.md contains a link to "Programming in Lean", which is now dead. I don't know whether "Programming in Lean" is still available somewhere, or whether it has been decided that it is too outdated to distribute. But I have a copy that I downloaded a while ago, so this is not an immediate issue for me.

[Chris Hughes]

environment.fold perhaps?

[Neil Strickland]

Thanks, that's probably what's required. It looks like it will need some monadic yoga to use it. I will try to work it out.

[Mario Carneiro]

@Neil Strickland Programming in Lean is half done and out of date, and it is currently going through some restructuring. I think Simon plans to fill in several more chapters. It is currently available at https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf (same place as before, just without the link on the main page), or on github at https://github.com/avigad/programming_in_lean