Zulip Chat Archive

Stream: general

Topic: non-persistent attributes


view this post on Zulip Simon Hudon (Jan 26 2019 at 22:33):

I'm trying to set an attribute inside a proof script and as soon as the proof is done, the attribute seems to disappear. Is this the desired behavior? Is there a way to make the attribute persistent?

view this post on Zulip Mario Carneiro (Jan 26 2019 at 23:01):

Theorems can't make permanent modifications to the environment, because they are executed out of order

view this post on Zulip Simon Hudon (Jan 26 2019 at 23:05):

Arrrrgh! I'm trying to generate unique file names for caching proof witnesses

view this post on Zulip Simon Hudon (Jan 26 2019 at 23:06):

Maybe I should just hash the goal


Last updated: May 10 2021 at 00:31 UTC