Zulip Chat Archive

Stream: new members

Topic: Running simp on the whole context


view this post on Zulip Guilherme Espada (Mar 10 2021 at 10:08):

Is there a way to run simp on the whole local context at once? Instead of having to do
simp at a,simp at b
being able to do something like
simp at all

view this post on Zulip Damiano Testa (Mar 10 2021 at 10:12):

simp at * should work.

view this post on Zulip Damiano Testa (Mar 10 2021 at 10:13):

In case it helps in other situations, simp at a ⊢ applies simp at a and at the goal. The symbol ⊢ is typed as \|-.

view this post on Zulip Guilherme Espada (Mar 10 2021 at 10:14):

Thanks! very helpful!

view this post on Zulip Marcus Rossel (Mar 11 2021 at 15:49):

You can also type the goal symbol as \go which might be easier :upside_down:


Last updated: May 11 2021 at 23:11 UTC