## Stream: new members

### Topic: nonterminal simp

#### Kevin Lacker (Oct 12 2020 at 23:08):

What's wrong with a nonterminal simp? Is there a doc on this somewhere?

#### Pedro Minicz (Oct 12 2020 at 23:10):

The problem with nonterminal simp is that if new lemmas that match the goal get annotated with @[simp] then the goal will be further reduced, possibly breaking the proof that followed.

#### Yury G. Kudryashov (Oct 12 2020 at 23:10):

It's hard to maintain.

ahh i see

#### Pedro Minicz (Oct 12 2020 at 23:10):

Terminal simp isn't a problem @[simp] tags getting removed from lemmas probably won't happen.

#### Kevin Lacker (Oct 12 2020 at 23:11):

what happens if a nonterminal simp is used and it breaks this way - would it get rejected by continuous integration?

#### Pedro Minicz (Oct 12 2020 at 23:16):

I hope yes. A silent failure would be worse.

#### Yury G. Kudryashov (Oct 12 2020 at 23:23):

Yes, it gets rejected by CI.

#### Bryan Gin-ge Chen (Oct 12 2020 at 23:45):

We have a page on simp on the community webiste with a section about why nonterminal simps are bad. We should probably add a line or two to the style guide too, though.

#### Kevin Lacker (Oct 13 2020 at 04:08):

I see - yeah I googled for "terminal simp" and "nonterminal simp" but didn't find that doc because its terminology is a bit different

#### Kevin Lacker (Oct 13 2020 at 04:09):

is there some vscode and/or emacs command to automatically replace a simp with its simp only form? or do people generally paste it in from some squeeze_simp output display?

#### Bryan Gin-ge Chen (Oct 13 2020 at 04:11):

In VS Code, the "Try this:" output from squeeze_simp becomes a link that can be clicked to replace simp with simp only.

#### Kevin Lacker (Oct 13 2020 at 04:12):

ok. that is by default available in a hover in emacs - does any emacs user happen to know what the name of that buffer is, so it can be explicitly opened?

#### Kyle Miller (Oct 13 2020 at 05:01):

Kevin Lacker said:

ok. that is by default available in a hover in emacs - does any emacs user happen to know what the name of that buffer is, so it can be explicitly opened?

You first need to create the window with C-c C-n (Lean menu: "Toggle next error display"). Then it's called *Lean Next Error*

Last updated: May 11 2021 at 22:14 UTC