Topic: Lean 3.22.0c
Bryan Gin-ge Chen (Oct 27 2020 at 00:43):
Today, we bid farewell to
decidable_linear_order, as Lean 3.22.0c is here! Thanks to @Eric Wieser, @Julian Berman, @Kevin Lacker and @Yury G. Kudryashov for their contributions (and @Gabriel Ebner and @Mario Carneiro for reviewing and merging their PRs)!
- Fix typos in docstrings for
lean --doc(which never actually did anything) (lean#480)
Mathlib PR: #4762 (awaiting-review)
Johan Commelin (Oct 27 2020 at 10:52):
Shall we merge the mathlib PR?
Kevin Buzzard (Oct 27 2020 at 11:21):
I'm looking at it now -- it's quite funny! I'm very pleased the section names have also been changed :-)
Kevin Buzzard (Oct 27 2020 at 11:23):
alias compares_swap ↔ ordering.compares.of_swap ordering.compares.swap mean?
Kevin Buzzard (Oct 27 2020 at 11:29):
Anne has some observation about spaces which should probably be incorporated
Yury G. Kudryashov (Oct 27 2020 at 11:34):
ordering.compares.swap lemmas as aliases for
iff.mpr parts of the
Kevin Buzzard (Oct 27 2020 at 11:36):
I'm glad to see that you struggled to find it as much as I did :-)
Kevin Buzzard (Oct 27 2020 at 11:48):
I made one trivial comment about square brackets and will now add to the list of thumbs-ups.
Yury G. Kudryashov (Oct 27 2020 at 11:55):
Last updated: May 14 2021 at 03:27 UTC