Zulip Chat Archive

Stream: general

Topic: Un-including an include


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

view this post on Zulip Patrick Massot (Sep 29 2018 at 10:52):

omit blah

view this post on Zulip Patrick Massot (Sep 29 2018 at 10:52):

and then reinclude

view this post on Zulip Keeley Hoek (Sep 29 2018 at 11:14):

awesome cheers!

view this post on Zulip Keeley Hoek (Sep 29 2018 at 11:15):

how about turning a list α into an expr?

view this post on Zulip Mario Carneiro (Sep 29 2018 at 11:21):

I think reflect is what you want?

view this post on Zulip Keeley Hoek (Sep 29 2018 at 11:32):

Sweet!

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

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

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

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

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