experiment: type improvements

[hargoniX]

No description provided.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 6c46c17 against 78df48b are in! @hargoniX

• 🟥 build//instructions: +8.5G (+0.07%)

Medium changes (1🟥)

• 🟥 riscv-ast.lean//instructions: +952.6M (+0.94%)

Small changes (1✅, 3🟥)

• ✅ binarytrees.st//instructions: -4.2M (-0.01%)
• 🟥 build/module/Init.Data.Order.PackageFactories//instructions: +31.0M (+0.48%)
• 🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt//instructions: +72.0M (+0.35%)
• 🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt//instructions: +53.8M (+0.36%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 78df48bdf4095e4a3b1dfda416bb3318aa0abfd7 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-20 23:49:02)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 78df48bdf4095e4a3b1dfda416bb3318aa0abfd7 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-20 23:49:03)