Zulip Chat Archive
Stream: mathlib4
Topic: Union notation
Yury G. Kudryashov (Jan 20 2023 at 23:06):
Lean shows ⋃ i, s i as unionᵢ _ in the output for me. How do we fix this? (I use emacs)
Yury G. Kudryashov (Jan 23 2023 at 08:23):
ping here.
Last updated: Dec 20 2023 at 11:08 UTC