subst and local constant expression

Stream: general

[Sean Leather]

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]

yeah I petitioned for this but leo said no

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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