Zulip Chat Archive

Stream: new members

Topic: Namespaces

Dean Young (Aug 11 2023 at 20:56):

What is a namespace? Is it ever essential to add "namespace CategoryTheory"? What does this function do, and will CategoryTheory.Cat ever function out of the namespace CategoryTheory?

namespace CategoryTheory

Eric Wieser (Aug 11 2023 at 20:57):

Why did you post this in #rss?

Notification Bot (Aug 11 2023 at 20:58):

This topic was moved here from #rss > Namespaces by Eric Wieser.

Dean Young (Aug 11 2023 at 21:04):

I forgot to name it.

Kevin Buzzard (Aug 11 2023 at 22:27):

Just look up namespaces in the manual.

Last updated: Dec 20 2023 at 11:08 UTC