documenting mathlib

[robertylewis]

We have instituted new documentation requirements for mathlib additions: https://github.com/leanprover-community/mathlib/pull/1229

It is a long term effort to bring the existing mathlib code base up to these standards. New pull requests will be responsible for updating parts of the library that they touch, within reason. But we strongly encourage everyone to add documentation for parts of the library they have created or are familiar with.

The following files have no headers at all:

• category_theory/sparse.lean
• category_theory/elements.lean
• category_theory/instances/rel.lean
• algebra/Mon/colimits.lean
• category/monad/basic.lean
• category/bitraversable/lemmas.lean
• category/bitraversable/instances.lean
• data/stream/basic.lean
• tactic/elide.lean
• topology/algebra/open_subgroup.lean

But at the moment, nearly all of mathlib needs updating. So pick a random file and there's likely work to be done.

A useful tool: the #doc_blame #lint only doc_blame user command prints all definitions above it in the current file that are missing doc strings. doc_blame! includes theorems and lemmas.

Update, April 4, 2020

#lint shows missing documentation now, instead of #doc_blame. All linter failures in the library can be seen here: https://github.com/leanprover-community/mathlib/blob/master/scripts/nolints.txt

Update, Dec 6, 2021

We've made good progress. Here is a list of style exceptions, including files that are missing module docs. Every file has at least a copyright header.

[kim-em]

I addressed some of these in #1264.

[cipher1024]

I should probably take care of

• [ ] category/monad/basic.lean
• [ ] category/bitraversable/lemmas.lean
• [ ] category/bitraversable/instances.lean