Zulip Chat Archive

Stream: general

Topic: Overnamespacing


Yaël Dillies (Jan 26 2022 at 19:02):

Having typeclasses and defs in namespaces (as opposed to just lemmas), as is done in category theory, ends up giving us some stupid names, like docs#category_theory.bundled_hom.category_theory.bundled.category_theory.concrete_category

Could we make it so that instances only get the namespace once?

Eric Rodriguez (Jan 26 2022 at 19:02):

can you even type that without the linter having a fit?

Yaël Dillies (Jan 26 2022 at 19:03):

Just about! It's 86 characters long.


Last updated: Dec 20 2023 at 11:08 UTC