Un-including an include

Stream: general

[Keeley Hoek]

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]

omit blah

[Patrick Massot]

and then reinclude

[Keeley Hoek]

awesome cheers!

[Keeley Hoek]

how about turning a list α into an expr?

[Mario Carneiro]

I think reflect is what you want?

[Keeley Hoek]

Sweet!

[Keeley Hoek]

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

[Kevin Buzzard]

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

[Keeley Hoek]

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]

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]

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