Zulip Chat Archive
Stream: general
Topic: TPIL update
Patrick Massot (May 02 2018 at 21:31):
:tada: Jeremy updated TPIL to Lean 3.4.1! :tada:
Kevin Buzzard (May 02 2018 at 21:32):
This is great news. My summer students will be using Lean 3.4.1 and I'm sure they'll find this resource extremely valuable.
Patrick Massot (May 02 2018 at 21:33):
It uses Sebastian update live Lean with current mathlib (see https://leanprover.github.io/theorem_proving_in_lean/tactics.html#using-the-simplifier)
Patrick Massot (May 02 2018 at 21:34):
It also doesn't feature any weird nat type class example
Patrick Massot (May 02 2018 at 21:34):
https://leanprover.github.io/theorem_proving_in_lean/type_classes.html
Kevin Buzzard (May 02 2018 at 21:37):
inhabited is a great example to start with. It is very much like the basic examples that people might have seen from Haskell. Spring the nat surprise on them later :-)
Patrick Massot (May 02 2018 at 21:37):
There is no more nat surprise
Patrick Massot (May 02 2018 at 21:37):
It's gone forever
Kenny Lau (May 02 2018 at 21:38):
what is the nat surprise?
Chris Hughes (May 02 2018 at 21:41):
The example type class was nat, with one as an instance.
Patrick Massot (May 02 2018 at 21:41):
Miko de Amsterdamo (May 03 2018 at 13:39):
Thanks, a good time to re-read the chapter
Last updated: Dec 20 2023 at 11:08 UTC