discrete math book

Stream: Lean for teaching

[Alexandre Rademaker]

Hi @Kevin Sullivan , I am reading https://kevinsullivan.github.io/cs-dm-dev/index.html, a very nice introduction to Lean and proofs. It is definitely an interesting alternative to the Avigad book that I used in my last DM course. One thing that called my attention is that you haven't gone deep (in chapter 2) to the difference between #eval and #reduce. One particular puzzle to me is way

#reduce (λ n : ℕ, n + 1)

but

#eval (λ n : ℕ, n + 1)

does not. In contrast, the evaluation or reduction of an identifier bound to a lambda term always works.