expr): sectioning doc strings (#1723)

Commit

6 years ago

doc(docs/contribute, meta/expr): sectioning doc strings (#1723) * doc(docs/contribute, meta/expr): explain sectioning doc strings and show in practice * updates

References

#1723 - doc(docs/contribute, meta/expr): sectioning doc strings

Author

robertylewis

Committer

mergify[bot]

Parents

b46ef845

mathlib3 e68b2be5 - doc(docs/contribute, meta/expr): sectioning doc strings (#1723)

mathlib3
e68b2be5 - doc(docs/contribute, meta/expr): sectioning doc strings (#1723)