Zulip Chat Archive

Stream: new members

Topic: forgetting assumptions in goal


view this post on Zulip Chris M (Jun 29 2020 at 08:32):

Suppose we have a goal where we have a list of assumptions and need to prove something. But suppose that some of the assumptions are unnecessary, and so you want to remove them from the tactic goal because it's distracting. How does one do this? is there a tactic for this?

view this post on Zulip Johan Commelin (Jun 29 2020 at 08:34):

@Chris M clear

view this post on Zulip Chris M (Jun 29 2020 at 08:35):

Great!


Last updated: May 14 2021 at 22:15 UTC