Zulip Chat Archive

Stream: Lean for teaching

Topic: Draft book using Lean for CS Discrete Math

Kevin Sullivan (Mar 04 2019 at 21:21):

Kevin Sullivan, I just noticed that at https://kevinsullivan.github.io/cs-dm-dev/02-Logic/Includes.html, in

Line 3 is a comment. Line 4 indicates that we’re defining a function called construct_a_proof.

and following, the line number references are all wrong.

Scott,, thank you, and thanks to the others, who have started to comment on this material. I've fixed most of the egregious problems that have been pointed out and will continue to do so. The material is updated on the web site. PDF generation will be working once all of the underlying materials are edited and pushed to the HTML web site. At that point, one will be able to print out something that actually resembles a book.

Kevin Sullivan (Mar 04 2019 at 21:22):

And thanks for launching this Lean-In-Teaching thread.

Patrick Massot (Mar 04 2019 at 21:25):

@Scott Morrison could you change the topic of the first message you posted in this topic?

Kevin Sullivan (Mar 04 2019 at 21:40):


Alexandre Rademaker (Sep 01 2019 at 13:48):

Any plans to continue the development of this material ?

Last updated: Dec 20 2023 at 11:08 UTC