Zulip Chat Archive

Stream: general

Topic: Terminology


Sebastien Gouezel (Feb 05 2019 at 13:15):

The following lemma is missing in the library

theorem to_nat_le_to_nat_of_le {a b : } (h : a  b) : to_nat a  to_nat b :=
by rw to_nat_le; exact le_trans h (le_to_nat b)

Should I call it to_nat_le_to_nat_of_le, or to_nat_mono? There are several lemmas named foo_mono in the library, but for uniformity I tend to prefer to_nat_le_to_nat_of_le (and I would be happy if all mono lemmas were renamed analogously). Strong opinions on this?

Mario Carneiro (Feb 05 2019 at 13:35):

I would go for to_nat_le, to_nat_le_to_nat, or to_nat_mono

Mario Carneiro (Feb 05 2019 at 13:35):

depending on whether there are any other reasonable similar theorems

Mario Carneiro (Feb 05 2019 at 13:37):

I'm not a fan of names that are considerably longer than needed for disambiguation

Sebastien Gouezel (Feb 05 2019 at 13:40):

OK, let's go for to_nat_le_to_nat (I don't like to_nat_mono because the natural thing to do is to start with to_nat_le and ask for autocompletion, which will fail).

Mario Carneiro (Feb 05 2019 at 13:43):

If it is a problem we can also have aliases, although we don't use them too often


Last updated: Dec 20 2023 at 11:08 UTC