Zulip Chat Archive

Stream: general

Topic: drop hypothesis from local context


view this post on Zulip Johan Commelin (May 25 2018 at 11:49):

Please remind me, which tactic removes hypotheses from the local context? Because I have used up some hyptheses, and I won't use them again, but the proof state is filling an entire screen.

view this post on Zulip Johan Commelin (May 25 2018 at 11:49):

I couldn't find the tactic in TPIL...

view this post on Zulip Sean Leather (May 25 2018 at 11:49):

clear

view this post on Zulip Johan Commelin (May 25 2018 at 11:50):

aah, thanks

view this post on Zulip Sean Leather (May 25 2018 at 11:50):

For reference: https://leanprover.github.io/reference/search.html?q=clear&check_keywords=yes&area=default

view this post on Zulip Johan Commelin (May 25 2018 at 11:50):

I see it is in TPIL, but the words "drop" or "remove" are not in its description

view this post on Zulip Sean Leather (May 25 2018 at 11:51):

You could try browsing this section if you're looking for something similar in the future.

view this post on Zulip Mario Carneiro (May 25 2018 at 11:51):

You can also use replace in place of have to clear old hyps as well

view this post on Zulip Sean Leather (May 25 2018 at 11:54):

I didn't know about replace.


Last updated: May 14 2021 at 07:19 UTC