Lean 3.19.0c

Stream: general

[Bryan Gin-ge Chen]

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

Features:

• There is a new option extends_priority which controls the priority of instances produced by extends. It is set to 100 by default. (lean#440)
• Add docs for the Lean server API (lean#443)

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)

Changes:

• 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]

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