Zulip Chat Archive

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

Keeley Hoek (Sep 29 2018 at 11:14):

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?

Keeley Hoek (Sep 29 2018 at 11:32):

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: Dec 20 2023 at 11:08 UTC