From 1f03e3252001a9a5cdfb354bfc45895d047bf4ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 Feb 2026 11:46:55 +0100 Subject: [PATCH] perf: inline the hash accessor of Name (#12583) This PR inlines the accessor for the computed hash field of `Name`. This ensures that accessing the value is basically always just a single load instead of doing a full function call. --- src/Init/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 6eded21d5f..acc1fc9d75 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -4685,7 +4685,7 @@ inductive Name where with /-- A hash function for names, which is stored inside the name itself as a computed field. -/ - @[computed_field] hash : Name → UInt64 + @[computed_field, inline] hash : Name → UInt64 | .anonymous => .ofNatLT 1723 (of_decide_eq_true rfl) | .str p s => mixHash p.hash s.hash | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatLT v h) (fun _ => UInt64.ofNatLT 17 (of_decide_eq_true rfl)))