naming bikeshed: `ofFoo`

Stream: mathlib4

[Arien Malec]

Although undocumented, I believe there's a naming convention that we name ofFoo toFoo etc.

1. Should this be documented in the wiki?
2. Should Topology.UniformSpace.Separation be updated to conform to the convention? (e..g., isClosed_of_spaced_out eq_of_separated_of_uniformContinuous)

[Jireh Loreaux]

Sorry, can you more explicitly specify what you think this undocumented naming convention is?

[Arien Malec]

Sure -- when we have a capitalized object, we often name projections or transformations to/from the object with a toFoo or ofFoo, but we are not consistent with that naming convention.

e.g., to_setoid -> toSetoid, to_finset -> toFinset

[Arien Malec]

but counterexamples above.

[Ruben Van de Velde]

Does it depend on whether Foo is a Prop(-ish)?

[Arien Malec]

I don't know? We ofFoo and toFoo sometimes and not others...

[Arien Malec]

I've got to believe there's some mathport support here, but I haven't code dived deeply enough yet.

Another example:

Why finprod_eq_prod_pLift_of_mulSupport_toFinset_subset in Algebra.BigOperators.Finprod? We have ofFinset but not ofMulSupport?

[Arien Malec]

I want to believe that if Foo is a name that gets an UpperCamelCase name also gets a toFoo/ofFoo name, but I haven't see it formalized that way.

[Yury G. Kudryashov]

toFinset is a definition, so we reuse it

[Yury G. Kudryashov]

Otherwise we insert _

[Yury G. Kudryashov]

This is a strange convention.

[Arien Malec]

Got it -- so to write back, I mistakenly pattern matched into a convention of is/of/toFoo because in Mathlib3 we do in fact have def and Prop-typed is/of/to_foos which get naming convention translated into IsFoo/toFoo, etc, but not always, so a theorem that expresses an invariance might be named of_Foo_toBar or ofFoo_toBar or etc., depending on whether there was an underlying definition or not.

I guess I don't then understand why we have Cycle.toFinset and Cycle.toFinset_toMultiset but also Cycle.nil_to_finset.

I'm coming at this from the perspective that it's good for naming conventions to have clear rules, and also good for the rules to be discoverable and consistent for an API user.

[Jireh Loreaux]

Have you seen the naming rules listed on the porting wiki? Eventually I think the naming convention will work its way into the website.

[Jireh Loreaux]

The nil one is just misnamed. You should open a PR to fix it.

[Arien Malec]

Jireh Loreaux said:

Have you seen the naming rules listed on the porting wiki? Eventually I think the naming convention will work its way into the website.

I wrote it...

[Arien Malec]

That's not quite correct, I edited it for clarity.

[Jireh Loreaux]

Anyway, there are a few toFinset things misnamed in that file.

[Arien Malec]

But most of my questions here are by way of making sure the rules are clear, and clearly documented...

[Eric Wieser]

I don't see it mentioned above; but the toFoo naming convention is automatically generated by Lean when using the extends keyword

[Eric Wieser]

Eg docs4#MulOneClass .toMul

[Arien Malec]

Jireh Loreaux said:

The nil one is just misnamed. You should open a PR to fix it.

!4#2057