Running simp on the whole context

Stream: new members

[Guilherme Espada]

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

[Damiano Testa]

simp at * should work.

[Damiano Testa]

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

[Guilherme Espada]

Thanks! very helpful!

[Marcus Rossel]

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