Kenny Lau (Nov 07 2018 at 20:43):
Can we make a tactic to forget the definition of something in the local context while keeping everything else unchanged?
Kenny Lau (Nov 07 2018 at 20:44):
so it would make
h : R := 1+1 into
h : R
Chris Hughes (Nov 07 2018 at 22:03):
generalize instead of let to define h in the first place. Is this something to do with trying to get
subst to work?
Kenny Lau (Nov 07 2018 at 22:11):
Mario Carneiro (Nov 08 2018 at 00:15):
replace h := h I think
Last updated: May 16 2021 at 22:14 UTC