Zulip Chat Archive

Stream: mathlib4

Topic: Name check

Arien Malec (Dec 27 2022 at 20:06):

In the port of Data.PNat.Find, I noted that where mathport had the name PNat.findX, it's called Nat.find_x in core

Should I follow core (current status), or use findX and file a ticket with core to deprecate Nat.find_x and add Nat.findX or just let the two diverge in naming?

Mario Carneiro (Dec 27 2022 at 20:09):

(it's not in core, it's in Mathlib.Init.Data.Nat.Lemmas)

Mario Carneiro (Dec 27 2022 at 20:09):

and it looks like it is just a really old file that predates the current consensus on the naming convention

Mario Carneiro (Dec 27 2022 at 20:13):

in particular, it looks like an ad hoc port file, it still needs a proper port

Arien Malec (Dec 27 2022 at 20:17):

Ah, mis-saw Init and thought core...

I'll rename in the PR, then maybe pick up that file.

Last updated: Dec 20 2023 at 11:08 UTC