Zulip Chat Archive
Stream: general
Topic: good names
Patrick Massot (May 13 2018 at 20:26):
I love it so much when I try to state a lemma and Lean complains the name is already used in mathlib (for the very same result I wanted to prove).
Last updated: May 02 2025 at 03:31 UTC