Zulip Chat Archive

Stream: new members

Topic: nonterminal simp


view this post on Zulip Kevin Lacker (Oct 12 2020 at 23:08):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 12 2020 at 23:10):

It's hard to maintain.

view this post on Zulip Kevin Lacker (Oct 12 2020 at 23:10):

ahh i see

view this post on Zulip Pedro Minicz (Oct 12 2020 at 23:10):

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

view this post on Zulip 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?

view this post on Zulip Pedro Minicz (Oct 12 2020 at 23:16):

I hope yes. A silent failure would be worse.

view this post on Zulip Yury G. Kudryashov (Oct 12 2020 at 23:23):

Yes, it gets rejected by CI.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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