[Merged by Bors] - chore(Geometry/Manifold): make some doc-strings follow the style guide#39729
[Merged by Bors] - chore(Geometry/Manifold): make some doc-strings follow the style guide#39729grunweg wants to merge 5 commits into
Conversation
b224b9b to
8cf19e5
Compare
PR summary 106ab480a9Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
@Vierkantor on the stylistic aspect (only if you'd like) |
8cf19e5 to
9dcaa53
Compare
|
This pull request has conflicts, please merge |
abb35a6 to
c2d5d9a
Compare
|
bors merge |
#39729) such as, by them beginning with the object they are defining as a subject. This will yield much better doc-strings for the differential geometry elaborators in #39677. It also increases conformance with the [documentation style guide](https://github.com/leanprover/lean4/blob/master/doc/style.md). Inspired by the MI retreat in Lisbon.
|
Pull request successfully merged into master. Build succeeded: |
such as, by them beginning with the object they are defining as a subject.
This will yield much better doc-strings for the differential geometry elaborators in #39677.
It also increases conformance with the documentation style guide.
Inspired by the MI retreat in Lisbon.