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: Dec 20 2023 at 11:08 UTC
(DELETED; I'm going to ask this differently)
Last updated: Dec 20 2023 at 11:08 UTC