Chapters that make no sense

Stream: lean4

[J. O.]

In the lean manual, sections 6 and 7 (expressions and declarations) make no sense whatsoever. They are poorly made, with no syntax highlighting and use copy-pasted examples from lean 3.

[J. O.]

I know the manual is wip, but the other sections are much cleaner and better. I wonder what is the cause for this “discrepancy”

[Arthur Paulino]

Lean 4 is not stable yet, so I think the manual can't be prioritized yet

[J. O.]

Arthur Paulino said:

Lean 4 is not stable yet, so I think the manual can't be prioritized yet

But that isn’t my concern. I’m wondering why those two extremely long sections are badly written. They should give a good gist, and not really complicated explanations. Honestly, i feel like those sections could be taken out completely, as they are explained more thourohly in other places

[Yury G. Kudryashov]

tl;dr: something is not done because no one (including you!) did it.

While a few people are actually paid to work on Lean, lots of stuff that happens around Lean is a community effort done by people who are not paid to work on Lean. And those who are paid to work on Lean answer to their bosses, not to you (or me). If some day MS will sell Lean 4 tech support to customers, then paying customers will have rights to ask for better manual/language/whatever.

[Patrick Stevens]

(Honestly I am perpetually shocked that Lean's documentation is as good as it is - it's first and foremost a research project, but its documentation is better than a lot of commercial software!)

[J. O.]

And dont get me wrong, I think the manual is really good, except for some parts

[J. O.]

thats all