Draft book using Lean for CS Discrete Math

Stream: Lean for teaching

[Kevin Sullivan]

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]

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

[Patrick Massot]

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

[Kevin Sullivan]

(deleted)

[Alexandre Rademaker]

Any plans to continue the development of this material ?