Zulip Chat Archive

Stream: general

Topic: Lean 3.19.0c

Bryan Gin-ge Chen (Aug 27 2020 at 15:48):

It's been almost a month since the last release, so I'm happy to announce Lean 3.19.0c! Thanks to @Yury G. Kudryashov, @Jannis Limperg, @Floris van Doorn, @Shing Tak Lam, @Reid Barton, @Mario Carneiro, @Rob Lewis, @Edward Ayers and @Johan Commelin for their contributions (and @Gabriel Ebner for reviewing and merging all their PRs)!


Bug fixes:

  • Fix name generation by injection_with (lean#430)
  • Fix bug in in_current_file (lean#432)
  • Fix docstring in introv (lean#434)
  • Fix parse precedence for #html (lean#444)
  • Add \fl and \fr to lstlean.tex (lean#448)


  • Avoid classical.choice in lt_of_le_of_ne (lean#428)
  • Remove usage of the axiom of choice from basic nat and int lemmas, remove private from internal lemmas about int and move the decidable.* order theorems from mathlib (lean#446)
  • Change syntax of guard_hyp from guard_hyp h := t to guard_hyp h : t and support guard_hyp h : t := val for checking let bindings (lean#445, lean#449)
  • Make fin a subtype (lean#452)

Mathlib PR: #3955 (draft)

Johan Commelin (Aug 27 2020 at 20:17):

This PR builds locally. There will probably be some simp linter warnings though.

Last updated: Aug 03 2023 at 10:10 UTC