Naming Conventions for Predicates

Stream: mathlib4

[Colin Jones ⚛️]

I am editing a pull request now that formalizes deficient, abundant, and weird numbers in Lean (#14269). My reviewer and I ran into an issue with the styling convention. Apparently, definitions like def Deficient should instead be written as def IsDeficient. However, Prime and Nat.Perfect do not follow this convention. Does anyone know what the right convention should be?

[Yaël Dillies]

See
Kevin Buzzard said:

When reviewing a PR adding things like abundant numbers I suggested they be called IsAbundant but then I realised that we had Prime and Perfect. I'd definitely be in favour of enforcing Is for Props, I think it makes for better understanding (for example it helps when trying to figure out how to make things like integral domains)

[Kyle Miller]

Clarification for myself: I think Yael is meaning to link to a thread with today's discussion about this, rather than saying that Kevin is saying what the convention is (that's still not exactly sorted out).

[Kevin Buzzard]

Yes there's at least one active discussion going on about this somewhere on this site (in a hurry and on mobile, sorry no link, but you can search for the quote above)

[Yaël Dillies]

Kyle is perfectly right. And in fact I agree more with Kyle than with Kevin in the aforementioned discussion.

[Yaël Dillies]

My internet connection is currently on and off, so don't expect my messages to always make sense