Zulip Chat Archive

Stream: general

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)!

Features:

Bug fixes:

  • Fix typos in docstrings for tactic.focus and tactic.focus' (lean#483)

Changes:

  • Remove lean --doc (which never actually did anything) (lean#480)
  • Add decidable_* assumptions to linear_order and remove decidable_linear_order (lean#484)

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):

What does 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):

https://leanprover-community.github.io/mathlib_docs/commands.html#alias
It creates ordering.compares.of_swap and ordering.compares.swap lemmas as aliases for iff.mp and iff.mpr parts of the iff lemma.

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):

bors merged

Last updated: May 02 2025 at 03:31 UTC