Zulip Chat Archive

Stream: general

Topic: TPIL update


view this post on Zulip Patrick Massot (May 02 2018 at 21:31):

:tada: Jeremy updated TPIL to Lean 3.4.1! :tada:

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Patrick Massot (May 02 2018 at 21:34):

It also doesn't feature any weird nat type class example

view this post on Zulip Patrick Massot (May 02 2018 at 21:34):

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html

view this post on Zulip 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 :-)

view this post on Zulip Patrick Massot (May 02 2018 at 21:37):

There is no more nat surprise

view this post on Zulip Patrick Massot (May 02 2018 at 21:37):

It's gone forever

view this post on Zulip Kenny Lau (May 02 2018 at 21:38):

what is the nat surprise?

view this post on Zulip Chris Hughes (May 02 2018 at 21:41):

The example type class was nat, with one as an instance.

view this post on Zulip Patrick Massot (May 02 2018 at 21:41):

https://github.com/leanprover/theorem_proving_in_lean/commit/b35ec10c142969d55123bb927980bee634734284

view this post on Zulip Miko de Amsterdamo (May 03 2018 at 13:39):

Thanks, a good time to re-read the chapter


Last updated: May 08 2021 at 03:17 UTC