Zulip Chat Archive
Stream: new members
Topic: how can i name a type Type?
JJ (Oct 12 2025 at 20:31):
I would like to name a type Type. Is there a way to trick the Lean namespaces into letting me do so?
Robin Arnez (Oct 12 2025 at 20:34):
You can name a type «Type» which is as close as it gets
JJ (Oct 12 2025 at 20:35):
Hmm, okay, bummer! I had thought there was some way to do this.
I'll either do that then or just call it Kind, I guess...
Last updated: Dec 20 2025 at 21:32 UTC