Zulip Chat Archive
Stream: lean4
Topic: nested namespaces
Paige Thomas (Feb 11 2025 at 05:30):
(deleted)
Paige Thomas (Feb 11 2025 at 05:32):
Oh, I thought I was making a new topic. Sorry, I didn't mean to attach this question to this existing topic.
Last updated: Dec 20 2025 at 21:32 UTC