[leodemoura]

This PR optimizes literal recognition and improves grind support for rational and signed fixed-width integer literals.

Replace value-extractor calls with direct Boolean checks. Add scientific Rat recognition and Int8/Int16/Int32/Int64 extraction and normalization. Fix interpretation of aliased types and handling of literals in match conditions. Add consistency tests covering wrapping, boundaries, metadata, and metavariables.

[leodemoura]

!bench

[leanprover-radar]

Benchmark results for 7b56476 against c9a3ebf are in. No significant results found. @leodemoura

• 🟥 build//instructions: +2.1G (+0.02%)

Small changes (7✅, 7🟥)

• 🟥 build/module/Lean.Compiler.LCNF.LambdaLifting//instructions: +6.1M (+0.22%)
• ✅ build/module/Lean.Meta.FunInfo//instructions: -8.7M (-0.45%)
• 🟥 build/module/Lean.Meta.LitValues//instructions: +1.3G (+35.99%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Meta.RecursorInfo//instructions: -4.7M (-0.17%)
• ✅ build/module/Lean.Meta.Tactic.BVDecide.Attr//instructions: -6.7M (-0.22%)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Internalize//instructions: +229.6M (+1.56%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Intro//instructions: +147.2M (+2.05%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Types//instructions: +336.8M (+1.15%) (reduced significance based on *//lines)
• ✅ build/module/Lean.PrettyPrinter.Delaborator//instructions: -191.2k (-0.03%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop//instructions: -2.4M (-0.26%)
• 🟥 build/module/Std.Http.Server//instructions: +3.2M (+0.18%)
• ✅ elab/bv_decide_inequality//instructions: -134.2M (-0.20%)
• 🟥 misc/leanchecker --fresh Init//maxrss: +5MiB (+0.94%)
• ✅ vcgen/GetThrowSetGrind/100/vcgen//wall-clock: -6ms (-7.64%)