Floris van Doorn (Jul 08 2019 at 11:29):
In the following code snippet, I add a declaration to the environment and then try to evaluate it. However, I get an error message stating that the declaration doesn't exist. Does
add_decl create VM code for the added declaration?
example : unit := by do let my_name : name := "foo", add_decl $ mk_definition my_name  `(unit) `(unit.star), -- get_env >>= λ env, trace $ env.contains my_name, decl ← mk_const my_name, -- eval_expr unit decl, eval_expr' unit decl, skip
Floris van Doorn (Jul 08 2019 at 11:46):
I have rewritten my code to work around this. My command adds a declaration to the environment if it doesn't exist yet, and in either case, then I do something with its value. I now rewrote the code so that I don't have to evaluate the newly added declaration. Evaluating a declaration added by a previous invocation of the command works fine.
Floris van Doorn (Jul 10 2019 at 14:11):
If someone finds this stream by searching: beware that if you write a command that adds a declaration to the environment if it doesn't exist yet (and then do something else), you will probably run into problems:
If file A and file B both add the same declaration to the environment, then file C which imports both of these files will raise the error that some declaration has been defined twice.
Last updated: May 18 2021 at 16:25 UTC