Zulip Chat Archive
Stream: lean4
Topic: doc additions
Julian Berman (Mar 06 2021 at 19:20):
Is opening tickets for things (e.g. syntax) not yet covered by the docs/manual (and also not seemingly marked with a TODO) useful or just noise?
Last updated: May 02 2025 at 03:31 UTC