naming conventions: LT.lt

Stream: mathlib4

[Filippo A. E. Nuccio]

In the naming convention page I find

-- follows rules 2 and 6
class LT (α : Type u) where
lt : α → α → Prop -- follows rule 4 and 6

and I do not understand: according to Rule 3, a function α → α → Prop should be named as terms in Prop, that is in UpperCamelCase by 2. Hence I would expect LT.LT (thorugh 6). What did I get wrong?

[A.]

This came up at least once before.

[A.]

It looks like I was supposed to make a PR to remove it from the examples list but never did.

[Filippo A. E. Nuccio]

Alistair Tucker said:

It looks like I was supposed to make a PR to remove it from the examples list but never did.

And are you going to? If not, I am happy to take care of it.

[A.]

Thanks, please do.

[Filippo A. E. Nuccio]

I have opened this PR with the modification, pinging @Jeremy Avigad for review.

[A.]

Did the naming conventions just get even more complicated?

[Eric Wieser]

I think this is an exception to the rule (it's LT.lt, Membership.mem, etc because core says so, not because that's the more general naming convention)