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: Dec 20 2023 at 11:08 UTC
Do exported definitions (usually, structure fields) need an additional #align? I guess so, right?
Last updated: Dec 20 2023 at 11:08 UTC