doc: add recommended spellings for many term notations #6886
Conversation
TwoFX
force-pushed
the
markus/recommended-spellings
branch
from
c02405c to
80f76d4
Compare
TwoFX
force-pushed
the
markus/recommended-spellings
branch
from
80f76d4 to
23e0105
Compare
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
| /-- not `isSuffix` -/ | ||
| recommended_spelling "suffix" for "<:+" in [IsSuffix, «term_<:+_»] |
There was a problem hiding this comment.
This goes against the community naming convention. Will there be a discussion about recommended spellings?
There was a problem hiding this comment.
Does it? There seems to be barely anything in mathlib about List.IsSuffix. https://loogle.lean-lang.org/?q=List.IsSuffix
There was a problem hiding this comment.
More generally, I have made an attempt to always use the established naming. If you think I made a mistake somewhere, feel free to note it here or start a thread on Zulip about specific spellings.
There was a problem hiding this comment.
suffix is the current name, but it goes against the naming convention (which would instead be isSuffix). I am worried that this recommended_spelling will turn the statu quo into an official recommendation.
There was a problem hiding this comment.
I don't think it is a problem if a notation has a different name than the declaration it refers to. For example, we say singleton for [x] and not something like consNil.
This PR adds recommended spellings for many notations defined in Lean core, using the `recommended_spelling` command from leanprover#6869.
This PR adds recommended spellings for many notations defined in Lean core, using the `recommended_spelling` command from leanprover#6869.
This PR adds recommended spellings for many notations defined in Lean core, using the
recommended_spellingcommand from #6869.