nonterminal simp

Stream: new members

[Kevin Lacker]

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

[Pedro Minicz]

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]

It's hard to maintain.

[Kevin Lacker]

ahh i see

[Pedro Minicz]

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

[Kevin Lacker]

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

[Pedro Minicz]

I hope yes. A silent failure would be worse.

[Yury G. Kudryashov]

Yes, it gets rejected by CI.

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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*