Zulip Chat Archive
Stream: lean4
Topic: Subsingleton.elim
Kevin Buzzard (Apr 02 2021 at 15:58):
In Lena 3 subsingleton.elim is a theorem. In Lean 4 it is a def. What is the reason for the change?
Sebastian Ullrich (Apr 02 2021 at 16:08):
There was no change, this was "fixed" in the community edition only. Also, Lena 3 has been deprecated in favor of Lane 5.
Last updated: May 02 2025 at 03:31 UTC