Generating web docs

Stream: condensed mathematics

[Eric Wieser]

Is there any interest in setting up doc-gen style documentation for lean-liquid? If so, I could PR some CI config to do so

[Eric Wieser]

(a side effect would be that https://eric-wieser.github.io/mathlib-import-graph could be used on it)

[Johan Commelin]

Thanks for the offer. We should certainly keep that in mind. I think that at the moment there are too many missing docstrings, and too much stuff that needs to be cleaned up, before being served via such an interface.