perf: better Char.toLower/Char.toUpper implementation

[hargoniX]

[hargoniX]

!bench

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for b4604799de17096e4e3470c76dfaffdca8af4e0a against ad02aa159c96aa78a01a5fff0e77413da3933094 are in! @hargoniX

Runs (2)

• 🟥 build exited with code -1
• 🟥 other exited with code -1

[leanprover-radar]

Benchmark results for 6eae00f312075e4fbf4d43c418136ae82e61ab2e against ad02aa159c96aa78a01a5fff0e77413da3933094 are in! @hargoniX

Major changes (1)

• ✅ workspaceSymbols//instructions: -707.9M (-2.6%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 3e4c2c6af9b88a35bf63c90bb638d7d2a208f332 against 59045c62276809a8b9cbc2a5f6904aeecf29dea7 are in! @hargoniX

Major changes (1)

• ✅ workspaceSymbols//instructions: -664.8M (-2.5%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 63a4aaaac72588135a639f77720b55155773825d against 59045c62276809a8b9cbc2a5f6904aeecf29dea7 are in! @hargoniX

Major changes (1)

• ✅ workspaceSymbols//instructions: -612.4M (-2.3%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 402ec6839b66d1728a9667d6731b57eb2b9cfd37 against 5339c47555cb65958259b1c4c4c687c3863a08be are in! @hargoniX

Major changes (2)

• ✅ charactersIn//instructions: -4.7G (-10.6%)
• ✅ workspaceSymbols//instructions: -608.7M (-2.3%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for bd394c45ecf0319df8f3872828388a79b6817b9d against 5339c47555cb65958259b1c4c4c687c3863a08be are in! @hargoniX

Major changes (2)

• ✅ charactersIn//instructions: -2.5G (-5.6%)
• ✅ workspaceSymbols//instructions: -496.8M (-1.9%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for d29deec7cc307bbeac0b2545a3bb404850a544ba against 95a7c769d8d1565fdafd32553bb44d7d53edf5c3 are in! @hargoniX

Major changes (2)

• ✅ charactersIn//instructions: -4.8G (-10.8%)
• ✅ workspaceSymbols//instructions: -679.5M (-2.6%)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-12-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-16 16:05:21)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-16 16:05:23)