Zulip Chat Archive

Stream: general

Topic: noob "resuse variable name" question


view this post on Zulip Kevin Buzzard (Sep 16 2018 at 10:07):

Dammit I can never remember how to go from H : P and HPQ : P -> Q to H : Q in tactic mode, the point being that I want to throw the original H away and reuse the name. There's a tactic that does this but I can never remember the name and I can't come up with an algorithm to find out for myself, my searches have been futile, so sorry, I have to ask.

view this post on Zulip Chris Hughes (Sep 16 2018 at 10:22):

specialize or replace

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 10:32):

replace -- that was it. I knew it was something like rewrite. Thanks.


Last updated: May 12 2021 at 04:19 UTC