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: May 16 2021 at 21:11 UTC