Zulip Chat Archive

Stream: general

Topic: blank parts of manual


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Apr 13 2020 at 19:15):

I guess ask question here.

view this post on Zulip Andrew Ashworth (Apr 13 2020 at 19:15):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 13 2020 at 19:21):

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

view this post on Zulip 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