Zulip Chat Archive
Stream: mathlib4
Topic: export
Reid Barton (Jan 01 2023 at 19:21):
Do exported definitions (usually, structure fields) need an additional #align? I guess so, right?
Last updated: May 02 2025 at 03:31 UTC
Do exported definitions (usually, structure fields) need an additional #align? I guess so, right?
Last updated: May 02 2025 at 03:31 UTC