Zulip Chat Archive

Stream: general

Topic: substitutions in `expr`


view this post on Zulip Simon Hudon (Apr 17 2018 at 01:45):

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?

view this post on Zulip Simon Hudon (Apr 17 2018 at 01:47):

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 02:34):

kabstract is the core function that does this

view this post on Zulip Simon Hudon (Apr 17 2018 at 02:36):

Nice! Thanks!


Last updated: May 14 2021 at 06:16 UTC