Add \U00000000 notation for large unicode literals

[eric-wieser]

This matches Python and Rust

Read this section before submitting

• Ensure your PR follows the External Contribution Guidelines.
• Please make sure the PR has excellent documentation and tests. If we label it missing documentation or missing tests then it needs fixing!
• Include the link to your RFC or bug issue in the description.
• If the issue does not already have approval from a developer, submit the PR as draft.
• The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
• A toolchain of the form leanprover/lean4-pr-releases:pr-release-NNNN for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing release-ci on its own line.
• If you rebase your PR onto nightly-with-mathlib then CI will test Mathlib against your PR.
• You can manage the awaiting-review, awaiting-author, and WIP labels yourself, by writing a comment containing one of these labels on its own line.
• Remove this section, up to and including the --- before submitting.

---

Closes #0000 (RFC or bug issue number fixed by this PR, if any)

[kmill]

One thing missing is a check that this is less than 0x110000 and not in the range [0xd800, 0xdfff]. That said, there's a missing check for u that it's not in the surrogate range [0xd800, 0xdfff]. Right now, '\ud800' gives '\x00'.

[eric-wieser]

Right now, '\ud800' gives '\x00'

I guess this is related to #5445. Is Char.ofNat 0xd80f = 0 really desirable? Python seems to make a different choice here.

[kmill]

Python passes these pairs through, right? And "\U00110000" is a syntax error?

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1b4ee185e879dddc6c50976b9467c16e9b0f864b --onto e551a366a0bbb27d5f853cc8e87cbd381a76ffc0. (2024-09-24 01:36:07)

[digama0]

Can we have rust's variadic syntax \u{12abc} instead? That would avoid the need to take more escape code letters. (This is also a way of saying that your "and Rust" is incorrect - this is not how rust does unicode escapes.)

[eric-wieser]

Doesn't rust support both \U00123456 and \u{123456}?

[digama0]

nope, "\U00123456" yields Syntax Error: unknown character escape. Rust doesn't have the \u1234 form either, the only accepted forms are \x12 and \u{123}.