feat: add basic byte order support

[fgdorais]

No description provided.

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 🟡 Mathlib branch batteries-pr-testing-1811 build against this PR was cancelled. (2026-05-18 04:31:49) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 🟡 Mathlib branch batteries-pr-testing-1811 build this PR didn't complete normally. (2026-05-18 04:47:20) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 🟡 Mathlib branch batteries-pr-testing-1811 build against this PR was cancelled. (2026-05-18 04:48:46) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 🟡 Mathlib branch batteries-pr-testing-1811 build against this PR was cancelled. (2026-05-18 04:56:26) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1811 has successfully built against this PR. (2026-05-18 05:51:48) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 🟡 Mathlib branch batteries-pr-testing-1811 build against this PR was cancelled. (2026-05-18 06:44:30) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1811 has successfully built against this PR. (2026-05-18 07:37:33) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1811 has successfully built against this PR. (2026-05-18 15:32:14) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1811 has successfully built against this PR. (2026-05-19 10:43:11) View Log

[wrenna-robson]

This looks basically sensible to me and useful to have. However, I would feel more comfortable if there were some checks on all the definitions you've made - either with appropriately chosen theorems, or I suppose an addition to test suites. The actual endianness check feels a little hacky but so does every endianness check I've ever seen, so probably no issue.

[fgdorais]

I have no idea why precompileModules = true breaks the seq_focus and simp_trace tests.

[fgdorais]

I've added a bunch of theorems. I probably missed some. I still have no clue why the tests are broken.

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch batteries-pr-testing-1811 build failed against this PR. (2026-05-21 04:07:20) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch batteries-pr-testing-1811 build failed against this PR. (2026-05-21 05:30:57) View Log

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch batteries-pr-testing-1811 build failed against this PR. (2026-05-21 06:44:31) View Log

[kim-em]

Could you say something about what this is for? I wasn't aware that endian-ness was a live issue anymore. :-)

[fgdorais]

I meant this to stay WIP. While my primary purpose was to test whether extern c inline would even work here, there are some applications. For example, to properly encode/decode a utf16 or utf32 string, one must pay attention to the byte-order mark (BOM) and adapt. It's also important to properly verify some transmission protocols. You're right though, this is not a concern in many higher level languages where low-level stuff is handled behind the scenes by the compiler. This is true for Lean except for that verification is important in order to trust the compiler.