Zulip Chat Archive
Stream: lean4
Topic: Bug in `incQuotDepth`?
Siddharth Bhat (Mar 31 2022 at 11:54):
(DELETED; I'm going to ask this differently)
Last updated: Feb 28 2026 at 14:05 UTC
(DELETED; I'm going to ask this differently)
Last updated: Feb 28 2026 at 14:05 UTC