Patrick Massot

I don't think it's worth making that code much more complicated for one example where we could simply change to "completeness of $l^2$" and "completeness of $L^2$"

Thanks for your amazing efforts with this list Johan!

I'm sorry I don't understand what you mean.

I have no idea what this issue means. The file you are quoting is indeed pretty hard to find since it targets very specific users who want to understand implementation...

Technically leanpkg is released with each Lean release but nobody works on it.

I don't understand the placement of those paragraph, and I don't understand the last sentence. And I'm skeptical about the general idea. People who arrive at those web page already...

I am closing this since it did not converge.