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: Dec 20 2023 at 11:08 UTC