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)!
- Options are refreshed when the simplifier is entered. (lean#456)
- JSON support for widgets (lean#453)
- More definition and theorem docstrings (lean#463)
- Typeclass args for
monad_state_transwere flipped. (lean#461)
nat.powfrom 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: May 10 2021 at 18:22 UTC