Zulip Chat Archive

Stream: general

Topic: subst and local constant expression

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?

Mario Carneiro (Feb 27 2018 at 09:01):

yeah I petitioned for this but leo said no

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

Mario Carneiro (Feb 27 2018 at 09:03):

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

Simon Hudon (Feb 27 2018 at 09:06):

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

Last updated: Aug 03 2023 at 10:10 UTC