Docstrings

[EdAyers]

I don't think this is ready to be merged yet. But here is my attempt to document Lean as I underwent the journey of understanding how it works. Maybe with some help from the community it can be made mergeworthy without too much effort.

Things that need to happen before this should be merged:

• How should later lines in the docstring be intented? This is complicated by how vscode interprets markdown, sometimes if you get the intenting wrong everything will be in a code block or bulleted lists don't get escaped
• Someone (possibly me) needs to check that my interpretations are correct. I have tried to read directly from the C++ whenever something isn't clear but I haven't doublechecked everything.
• The documentation is incomplete, I stuck to only documenting things where it is not clear what it does from the name and type signature. I don't think documenting absolutely every declaration is a good use of anyone's time, but having docstrings for non-obvious things saves time for users in the long-run.

[khoek]

I fixed one of the two failing tests in a pull request, but the other has a [TODO] in it so I didn't touch it.

[khoek]

Boo-hoo on the last build failure, but I'm pretty sure that that was caused by bad luck and not a test failure.