## Stream: general

### Topic: a tactic to forget the definition

#### 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):

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

it isn't

#### Mario Carneiro (Nov 08 2018 at 00:15):

you could replace h := h I think

Last updated: May 16 2021 at 22:14 UTC