docs(category/monad,bitraversable): add module docstrings #1260

[cipher1024]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[cipher1024]

See #1260

[robertylewis]

Thanks. This is a good start, but I'm afraid the comments mean very little to me as is. Maybe a good place to start would be documentation for bitraversable.basic? Could you take this opportunity to add declaration doc strings too?

[robertylewis]

Thanks for the additions, but I'd still like to see more. Right now I don't know what bitraversable is or what I would use these files for. Again, the solution might just be to document bitraversable.basic and relate these comments to there.

[cipher1024]

@robertylewis Before I add a docstring there, do you understand what traversable does? That might be what needs clarification.

[robertylewis]

Clarifying both would be very helpful!

[cipher1024]

Would the new comment on bitraversable work for traversable? Do you need more information than that?

[robertylewis]

What I would like from the module docs is to be able to understand the purpose of a file and if/how I might use its contents, without looking through the whole file itself. Some amount of back-referencing is unavoidable, e.g. the p-adic integers doc doesn't repeat everything about the p-adic numbers. But the more of this there is, the harder it is to read, and it shouldn't be necessary to look up external references to get the general idea of a mathlib file.

I'm being picky here because this seems like a programming tool instead of/as well as a mathematical theory. This could be useful for people programming in Lean, but without clear explanations of what it does, they'd never know.