Zulip Chat Archive

Stream: general

Topic: Lean 3.17.0

view this post on Zulip Gabriel Ebner (Jul 06 2020 at 14:32):

Let's bump the minor version number again! This week we can welcome the 3.17.0 release of the Lean community edition! Thanks to @Edward Ayers, @Scott Morrison, @Floris van Doorn, @Johan Commelin!


Bug fixes:


  • Fix vacuous assumptions in nat lemmas (lean#366)
  • Remove has_neg instance for set (lean#367)
  • Mark dif_ctx_congr as @[congr] (lean#378)

Server protocol changes:

  • The response of the widget_event request may now contain effects.

Mathlib PR:

Last updated: May 15 2021 at 00:39 UTC