Zulip Chat Archive

Stream: mathlib4

Topic: mathport import naming


Maxwell Thum (Jan 13 2023 at 22:01):

It seems that mathport is writing import Mathlib.Data.Set.Pointwise.Smul when it should be writing import Mathlib.Data.Set.Pointwise.SMul. I know this is an easy fix, but is it cause for concern? Is this issue specific to the way we've named SMul?

Eric Wieser (Jan 13 2023 at 22:06):

This probably came up for ENat vs Enat too. Perhaps we need some kind of #align_filename command to prevent all the downstream imports needing fixing?


Last updated: Dec 20 2023 at 11:08 UTC