Zulip Chat Archive

Stream: Lean for teaching

Topic: discrete math book

Alexandre Rademaker (May 02 2020 at 22:16):

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)


#eval (λ n : , n + 1)

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

Last updated: Dec 20 2023 at 11:08 UTC