Pierre Vial (Sep 04 2020 at 09:47): Pierre Vial (Sep 04 2020 at 09:47):Hello,
Is there a MetaCoq function that just quotes thecurrent global environment?
I would expect its type to be global_env or global_env_ext
Théo Winterhalter (Sep 04 2020 at 11:50):Hi,
I think you can only get the environment on which depends a definition, it would otherwise get too big, containing the whole standard library for starters.
Théo Winterhalter (Sep 04 2020 at 11:51):You get the environment by adding Recursively after Quote.
Pierre Vial (Sep 04 2020 at 12:25):Ok, thanks!
Last updated: Nov 29 2023 at 05:01 UTC