Zulip Chat Archive

Stream: new members

Topic: PR Sublattice

Matúš Behun (Apr 07 2021 at 20:33):

Anybody willing to look at talk about my PR? I am trying to define order/sublattice. I need at least some quick overview if structure is right and what else should I work on to be successful with merge.

#7093

Johan Commelin (Apr 07 2021 at 20:39):

@Matúš Behun welcome! (Note that there is a dedicated stream #PR reviews for discussion of specific PRs.)

Kevin Buzzard (Apr 07 2021 at 20:39):

Thanks for doing this! PR's have their own stream -- perhaps we should continue this conversation in #PR reviews .

Kevin Buzzard (Apr 07 2021 at 20:39):

heh :-)

Johan Commelin (Apr 07 2021 at 20:40):

First look: this looks pretty good, but there are some style issues.

Johan Commelin (Apr 07 2021 at 20:40):

@Matúš Behun please take a look at https://leanprover-community.github.io/contribute/style.html#structuring-definitions-and-theorems

Eric Wieser (Apr 07 2021 at 20:54):

A zulip admin can presumably move this thread?

Notification Bot (Apr 07 2021 at 21:38):

This topic was moved by Mario Carneiro to #PR reviews > sublattice definition #7093

Last updated: Dec 20 2023 at 11:08 UTC