Commit 2024-12-26 07:24 9adbe92f

View on Github →

docs: fix typos across repository (#20239) Supercedes https://github.com/leanprover-community/mathlib4/pull/20236. Hopefully this stops a few typos pull requests later. Uses crates-ci/typos, with the following config:

[default.extend-words]
# keywords & abbreviations
pn = "pn"
hae = "hae"
hom = "hom"
mor = "mor"
thm = "thm"
tpos = "tpos"
hpe = "hpe"
fle = "fle"
eis = "eis"
iy = "iy"
hge = "hge"
alls = "alls"
struc = "struc"
onl = "onl"
hav = "hav"
hax = "hax"
ba = "ba"
ein = "ein"
adn = "adn"
loopup = "loopup"
hsa = "hsa"
dum = "dum"
mapp = "mapp"
nd = "nd"
ist = "ist"
haa = "haa"
ot = "ot"
comon = "comon"
ihs = "ihs"
thr = "thr"
projectives = "projectives"
hda = "hda"
ane = "ane"
hsi = "hsi"
minimals = "minimals"
ninj = "ninj"
ue = "ue"
tne = "tne"
lits = "lits"
ine = "ine"
tre = "tre"
fo = "fo"
nam = "nam"
larg = "larg"
reord = "reord"
nin = "nin"
toi = "toi"
ands = "ands"
hte = "hte"
strat = "strat"
hink = "hink"
lastr = "lastr"
wth = "wth"
iin = "iin"
# deprecations based on typos
continous = "continous"
# names and non-english words
falso = "falso"
yoh = "yoh"
tak = "tak"
lacker = "lacker"
fonctions = "fonctions"
calle = "calle"
gool = "gool"
sur = "sur"
periodes = "periodes"
waring = "waring"
espaces = "espaces"
yau = "yau"
topologie = "topologie"
claus = "claus"
parth = "parth"
ines = "ines"
fike = "fike"
tunnell = "tunnell"
groupes = "groupes"
htmp = "htmp"
ket = "ket"
clos = "clos"
abd = "abd"
# typo that i'm worried about breaking
conciousness = "conciousness" # part of a test
assum = "assum" # this might just be an abbrv but it's in a tactic and not used anywhere else
[files]
extend-exclude = ["docs/references.bib"]

I've dropped this config from this PR, but these typos ran across the repository - it may be beneficial for there to be CI to stop these unnecessary theorem deprecations. However, as the config also indicates, this captures a lot of false positives from the various abbreviations used.

Estimated changes