Marc Huisinga 2324c0939d chore: add private getUtf8Byte' to Init.Meta (#10140) ... This PR adds a private `Lean.Name.getUtf8Byte'` to `Init.Meta` for a future PR that optimizes `Lean.Name.escapePart`. `Lean.Name.getUtf8Byte'` should be replaced with `String.getUtf8Byte` once the string refactor is through.		2025-08-26 16:54:02 +00:00
..
src	chore: add private getUtf8Byte' to Init.Meta (#10140)	2025-08-26 16:54:02 +00:00
stdlib	chore: update stage0	2025-08-26 16:01:23 +00:00