Zulip Chat Archive

Stream: general

Topic: subst and local constant expression


view this post on Zulip Sean Leather (Feb 27 2018 at 09:01):

Why does subst need its expression argument to be a local constant? I would like to be able to do something like subst <expr> with an arbitrary <expr>, but this results in:

error: subst tactic failed, given expression is not a local constant

Instead, I have to do:

have : a = b := <expr>, subst this

Is it because subst always clears the argument? Should there be a version of subst that doesn't clear?

view this post on Zulip Mario Carneiro (Feb 27 2018 at 09:01):

yeah I petitioned for this but leo said no

view this post on Zulip Mario Carneiro (Feb 27 2018 at 09:02):

it's an expr so you can use the french quotes to select a variable from the context by type

view this post on Zulip Mario Carneiro (Feb 27 2018 at 09:03):

You can do mostly the same thing with cases e where e : a = b

view this post on Zulip Simon Hudon (Feb 27 2018 at 09:06):

Otherwise, you may need to do generalize first and then subst.


Last updated: May 10 2021 at 00:31 UTC