Zulip Chat Archive

Stream: general

Topic: a tactic to forget the definition


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Nov 07 2018 at 20:44):

so it would make h : R := 1+1 into h : R

view this post on Zulip Chris Hughes (Nov 07 2018 at 22:03):

Use generalize instead of let to define h in the first place. Is this something to do with trying to get subst to work?

view this post on Zulip Kenny Lau (Nov 07 2018 at 22:11):

it isn't

view this post on Zulip Mario Carneiro (Nov 08 2018 at 00:15):

you could replace h := h I think


Last updated: May 16 2021 at 22:14 UTC