Topic: substitutions in `expr`
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?
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?
Mario Carneiro (Apr 17 2018 at 02:34):
kabstract is the core function that does this
Simon Hudon (Apr 17 2018 at 02:36):
Last updated: May 14 2021 at 06:16 UTC