mixin and data class names

Stream: general

[Yury G. Kudryashov]

Should we fix some naming convention for data and Prop-valued mixin classes?

[Yury G. Kudryashov]

E.g., we have docs#has_involutive_star (data) and docs#has_continuous_mul (prop mixin)

[Eric Wieser]

My preference would be to use is_ for Prop and has_ for Type, but that might be quite an invasive change.

[Eric Wieser]

Under that scheme, has_continuous_mul would become mul_is_continuous or is_continuous_mul

[Yaël Dillies]

What about continuous_mul_class on the model of smul_comm_class?

[Eric Wieser]

The _class suffix feels like noise to me - I'd lean towards trying to purge it as part of the same renaming

[Yaël Dillies]

is_comm_smul and is_assoc_smul, then?

[Eric Wieser]

Well is_scalar_tower already starts with is_ and avoids class, so no need to rename that to is_assoc_smul?

[Yaël Dillies]

But it's not a very descriptive name.

[Yaël Dillies]

I know you're trying to save your FMM paper from deprecation :stuck_out_tongue_closed_eyes:

[Moritz Doll]

I find the is_ convention really nice, but for some topology stuff it came up that is_compact is for sets so compact_space can only be renamed to is_compact_space and under that convention we would get stuff like is_locally_convex_space which is really long.

[Moritz Doll]

(and the _space is somewhat redundant)

[Kyle Miller]

I feel like this had been discussed before, but maybe not for classes. Two related threads:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60is_foo.60.20v.20.60foo.60/near/266509885
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Noun.2Fadjective.2Fverb.20naming.20conventions.20for.20defs.20in.20mathlib/near/206742747