Zulip Chat Archive

Stream: general

Topic: unknown declaration which I just added


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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