feat: convert docComments in Literate Lean pages

[pimotte]

This feature is controlled by the verso.literateMarkdown.convertDoccomments option, which defaults to false for backwards compatibility.

[david-christiansen]

This is making me think that this should be an attribute rather than a hardcoded list.

[pimotte]

Is there a way we can attach an attribute to the keyword lemma somehow (or can we avoid tagging every lemma in the book project)? If yes, I definitely agree.

If not, I think it depends on the aim of LiterateLeanPage:

• If the goal is to best-effort render any existing lean file, then having to tag the custom-definitions you want to be converted is kind of rough.
• If the goal is to provide an easy way to convert an existing lean file to something that can be rendered nicely, then I think introducing an attribute is fine.

I can totally get it if you don't want to have the hardcoded `lemma there in any case, so I'm also happy to remove it and maintain it as a patch right now for the analysis book project, since I'm currently doing that anyway.

[david-christiansen]

I was thinking that there would be something like an attribute that's attached to the syntax kind lemma, not to every lemma in the world! So you'd have something along the lines of:

attribute [renderDocComments] Mathlib.Parser.Declarations.lemma

once in your setup file.

Do you know how to make an environment extension and a custom attribute? If not, I can do that last step before merging.

[david-christiansen]

And it's not so much that I want to avoid the hardcoded lemma as it is that I want other people to be able to use this with their own custom syntax without having to send me patches!