Topic: blank parts of manual
Michael Beeson (Apr 13 2020 at 19:13):
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 (Apr 13 2020 at 19:15):
I guess ask question here.
Andrew Ashworth (Apr 13 2020 at 19:15):
Andrew Ashworth (Apr 13 2020 at 19:16):
Reference manual is not maintained, if you have deeper questions on Lean I would look at TPIL
Andrew Ashworth (Apr 13 2020 at 19:18):
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 (Apr 13 2020 at 19:18):
BTW, can we add a disclaimer "This manual is not maintained, see TPIL" to the manual?
Johan Commelin (Apr 13 2020 at 19:21):
@Jeremy Avigad Is it appropriate to ping you here? :up:
Jeremy Avigad (Apr 13 2020 at 19:54):
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.
Last updated: May 12 2021 at 05:19 UTC