## Stream: new members

### Topic: Running simp on the whole context

#### 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

#### Damiano Testa (Mar 10 2021 at 10:12):

simp at * should work.

#### 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 \|-.

#### Guilherme Espada (Mar 10 2021 at 10:14):

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