-
Notifications
You must be signed in to change notification settings - Fork 139
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
doc(Style): clarify indentation of documentation strings #596
base: lean4
Are you sure you want to change the base?
doc(Style): clarify indentation of documentation strings #596
Conversation
templates/contribute/style.md
Outdated
@@ -80,7 +80,8 @@ two main concepts in the theory of xyzzyology. | |||
## Main results | |||
|
|||
- `exists_foo`: the main existence theorem of `foo`s. | |||
- `bar_of_foo`: a construction of a `bar`, given a `foo`. | |||
- `bar_of_foo`: a construction of a `bar`, given a `foo` under very complicated | |||
and intricate circumstances worth describing in excruciating detail. |
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.
I don’t understand what this change is doing here.
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.
The change is meant to illustrate an example, where an item spans multiple lines. (I got this wrong previously, by not indenting the second line: this is not how markdown expects items. Hence, I think this is worth clarifying.)
It seems the wording is not clear; I'm very happy to change it. For instance, would this be clearer?
- `bar_of_foo_of_baz`: a construction of a `bar`, given a `foo` and a `baz`. If this doc-string was longer than one
line, subsequent lines should be indented by two spaces (as required by markdown syntax).
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.
This makes sense to me!
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.
I have updated the phrasing. @PatrickMassot Does that address your comment?
I searched for guidelines here, and could not find them. Zulip yields very clear rules; let's codify them.