## 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


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: May 10 2021 at 00:31 UTC