Markus Himmel 19bd0254c3 chore: move String.utf8EncodeChar to the prelude (#10264) ... This PR moves `String.utf8EncodeChar` to the prelude to prepare for the imminent redefinition of `String`. The definition in the prelude uses modulo and division operations on natural numbers. In `String.Extra`, a `csimp` lemma is provided, showing that the new definition is equal to the previous one (which is now called `utf8EncodeCharFast`) which uses bitwise operations on `UInt8`.		2025-09-07 12:42:53 +00:00
..
bench	perf: improve iterator/range benchmarks, use shortcut instances for Int ranges (#10197)	2025-09-03 15:47:52 +00:00
compiler	fix: Unicode path support for Lean Windows executables (#10133)	2025-08-27 11:28:55 +00:00
elabissues
ir
lean	chore: move String.utf8EncodeChar to the prelude (#10264)	2025-09-07 12:42:53 +00:00
pkg	perf: rebuild leak on private match (#10246)	2025-09-04 12:51:42 +00:00
playground	feat: linear-size DecidableEq instance (#10152)	2025-09-03 06:31:49 +00:00
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain