mathlib4
mathlib4 copied to clipboard
chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast`
Now that I am defining NNRat.cast
, I want a definitive answer to this naming issue. Plenty of lemmas in mathlib already use natCast
/intCast
/ratCast
over nat_cast
/int_cast
/rat_cast
, and this matches with the general expectation that underscore-separated name parts correspond to a single declaration.
Let's solicit a few more votes on https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/naming.20conventions.3A.20natCast.20vs.20nat_cast/near/346323810 first.
Seems like there's a majority in favour
Please make a PR to update the naming guide to explicitly record this clarification to the naming convention; if we're going to make this sweeping a change, we should make sure it's documented as the preferred naming convention.
https://github.com/leanprover-community/leanprover-community.github.io/pull/459
bors d+
:v: YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+
. More detailed instructions are available here.
bors merge
Pull request successfully merged into master.
Build succeeded: