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: Feb 28 2026 at 14:05 UTC
Do exported definitions (usually, structure fields) need an additional #align? I guess so, right?
Last updated: Feb 28 2026 at 14:05 UTC