blank parts of manual

Stream: general

[Michael Beeson]

Some parts of the Lean Reference Manual are completely blank, for example the section on class definitions.
So how am I supposed to fix my class definition that is erroneous?

[Yury G. Kudryashov]

I guess ask question here.

[Andrew Ashworth]

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html

[Andrew Ashworth]

Reference manual is not maintained, if you have deeper questions on Lean I would look at TPIL

[Andrew Ashworth]

Along with Programming in Lean it never got a lot of attention because it's really most appropriate for people trying to do program verification, but not many CS people switched from Agda or Coq to Lean

[Yury G. Kudryashov]

BTW, can we add a disclaimer "This manual is not maintained, see TPIL" to the manual?

[Johan Commelin]

@Jeremy Avigad Is it appropriate to ping you here? :up:

[Jeremy Avigad]

Sure, I'll update the opening pages of Programming in Lean and the Reference Manual to make it clear that they are not being updated or maintained. I apologize for the confusion.