Zulip Chat Archive

Stream: new members

Topic: Clear all

Bhavik Mehta (Dec 06 2019 at 19:25):

Is there some kind of clear all tactic, which will clear a hypothesis and everything depending on it?

Simon Hudon (Dec 06 2019 at 20:37):

From mathlib, you can use clear_except without arguments.

Bhavik Mehta (Dec 07 2019 at 09:39):

This clears too many hypotheses, I only want to remove all the things mentioning a specific variable/hypothesis

Last updated: Dec 20 2023 at 11:08 UTC