## Stream: general

### Topic: Un-including an include

#### Keeley Hoek (Sep 29 2018 at 10:52):

If include blah occurs in my current namespace, is there a way to make a special definition which doesn't take blah as an argument?

#### Patrick Massot (Sep 29 2018 at 10:52):

omit blah

#### Patrick Massot (Sep 29 2018 at 10:52):

and then reinclude

awesome cheers!

#### Keeley Hoek (Sep 29 2018 at 11:15):

how about turning a list α into an expr?

#### Mario Carneiro (Sep 29 2018 at 11:21):

I think reflect is what you want?

Sweet!

#### Keeley Hoek (Sep 29 2018 at 11:33):

Has anyone ever gotten the error VM does not have code for 'xyz.abc' after trying to use something they environment.added?

#### Kevin Buzzard (Sep 29 2018 at 11:37):

The only time I get that error is when I've accidentally used theorem to make a definition

#### Keeley Hoek (Sep 29 2018 at 12:04):

it turned out to be a really obscure problem, where if you call user_attribute.get_param with someone who doesn't have the attribute set, the vm un-gracefully shoots you down without a catchable fail

#### Keeley Hoek (Sep 29 2018 at 12:31):

If this ever comes up for anyone else, environment.add is a little messed up if you want to later add attributes
Instead use tactic.add_decl (both are implemented in C++)

#### Simon Hudon (Sep 29 2018 at 20:48):

it turned out to be a really obscure problem, where if you call user_attribute.get_param with someone who doesn't have the attribute set, the vm un-gracefully shoots you down without a catchable fail

Are you sure? get_param has issues because it uses eval_expr which is kind of broken. Try get_param_untyped instead to see if it crashes uglily, still

Last updated: May 08 2021 at 18:17 UTC