Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
Shall we change the name of `nat` to `Nat`?
Since I am cleaning up the nat library in #1469 it might be a good time to consider doing this.
The proposal is to change the name nat to Nat. This puts us more in line with our naming convention. What do you think?
I think it might be better to retain compatibility with the standard Coq library for this kind of thing (as much as possible). I often google things about nat in order to figure out the names of standard lemmas. But maybe so much is being revamped that the name of the type is a minor point?
The search results are case sensitive! :-) But more important than the case is renaming things like nat_add_comm vs nat_plus_comm, so my comment is really more generally about trying to stay compatible during the reorganization (unless there is a strong benefit to not staying compatible).
I think we will only rename the type nat to Nat whilst the lemmas nat_X will stay as they are since they are following convention.
Since we use the Coq names for various lemmas and I have no plans of coming up with our own nat conventions, it probably isn't worth the friction to rename nat here. If we do feel like we want to do something like this in the future, it would probably involve making all our stuff about nat more homogeneous with respect to the rest of the library. Therefore I am closing this issue.