Zulip Chat Archive

Stream: general

Topic: Lean 3.20.0c

Bryan Gin-ge Chen (Sep 10 2020 at 00:14):

It's time to say goodbye to nat.pow and hello to Lean 3.20.0c! Thanks to @Reid Barton, @Edward Ayers, @Chris B, @Simon Hudon and @Kevin Buzzard for their contributions (and @Gabriel Ebner for reviewing and merging their PRs)!

Features:

  • Options are refreshed when the simplifier is entered. (lean#456)
  • JSON support for widgets (lean#453)
  • More definition and theorem docstrings (lean#463)

Bug fixes:

  • Typeclass args for monad_state_trans were flipped. (lean#461)
  • resolve_constant now handles parameters correctly. (lean#462)

Changes:

  • Remove nat.pow from the core library (lean#457)

Mathlib PR: #3985 (WIP)

Kevin Buzzard (Sep 10 2020 at 06:01):

Bye bye nat.pow!

Jeremy Avigad (Sep 10 2020 at 20:01):

Alas, now we have to remove the annoying explanation of nat.pow in MiL... (I'll do it tomorrow.)

Johan Commelin (Sep 10 2020 at 20:12):

So long and thanks for all the pow...

Patrick Massot (Sep 10 2020 at 20:19):

This is a great day.

Alexandre Rademaker (Sep 11 2020 at 05:22):

I didn’t find any comment in MiL about the nat.pow. What is the problem with it?

Kevin Buzzard (Sep 11 2020 at 06:32):

There are two instances which lean can find and sometimes it finds both

Johan Commelin (Sep 11 2020 at 06:36):

And they aren't defeq

Last updated: Dec 20 2023 at 11:08 UTC