Zulip Chat Archive
Stream: new members
Topic: Namesapces at EoF
Treq (Dec 14 2023 at 19:41):
Does a namespace close itself at the end of a file, or should I be adding end <identifier> as the line line?
Kevin Buzzard (Dec 14 2023 at 19:42):
In Lean 4 it does, and people seem to use this in code in the wild.
Treq (Dec 14 2023 at 19:43):
Good to know, thanks!
Last updated: May 02 2025 at 03:31 UTC