unknown declaration which I just added

Stream: general

[Floris van Doorn]

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]

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]

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.