## Stream: general

### Topic: unknown declaration which I just added

#### 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