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: Dec 20 2023 at 11:08 UTC