-
Notifications
You must be signed in to change notification settings - Fork 115
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
update contribute/style #155
Conversation
These changes look great to me. In particular the comment that lower case greek letters should be used for "generic types" (but sensible maths capital letters can be used for sensible maths objects) is long overdue and I think fits very well with what is happening right now (and is also a good system!) |
LGTM. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me too!
As mentioned in the Zulip thread, I would prefer to not have the convention "a single tactic invocation per line". The rest LGTM. |
Should we change "We generally restrict the use of dots to inductive types." in |
I have also made a few changes to |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good, thank you!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me too. I'll merge it.
Based on a discussion with @fpvandoorn at leanprover-community/mathlib#5414 (comment), I have the impression that the style guide does not completely reflect our current style. I propose some modifications in the current PR based on my feeling of what these practices are. Feedback/improvements/clarifications are most welcome!