substitutions in `expr`

Stream: general

[Simon Hudon]

If I have e : expr and I have a pattern p : expr which I would like to substitute for a variable (a bit like generalize does for a proof goal) what is the best way to do it?

[Simon Hudon]

Is there something better than making a goal that contains e and calling generalize p on it?

[Mario Carneiro]

kabstract is the core function that does this

[Simon Hudon]

Nice! Thanks!