logic and proof: discussion

Stream: general

[Slavomir Kaslev]

Looks great, thanks for doing this!
The PDF link at the bottom of the page seems to be broken currently.

[Philippe Duchon]

(Not sure if this is the right place to discuss this?) There are also some code snippets that don't work right out when I "try it". At least the proof of irrationality of square root of 2 (in chapter 1) chokes on the import.

[Pietro Monticone]

Philippe Duchon said:

(Not sure if this is the right place to discuss this?) There are also some code snippets that don't work right out when I "try it". At least the proof of irrationality of square root of 2 (in chapter 1) chokes on the import.

I have fixed it yesterday (the correct file to be imported is Mathlib.Data.Nat.Prime.Basic). It doesn't show up at the moment because we haven't regenerated the book yet.

[Notification Bot]

3 messages were moved here from #announce > logic and proof by Johan Commelin.