From 88ecacea4e70162616a2c334e6e0488bfb78f73a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 19 Feb 2026 10:00:13 +0100
Subject: [PATCH] feat: make computed_fields respect inline (#12580)

This PR makes `computed_field` respect the inline attributes on the
function for computing the
field. This means we can inline the accessor for the field, allowing
quicker access.
---
 src/Lean/Elab/ComputedFields.lean | 7 +++++--
 stage0/src/stdlib_flags.h         | 2 ++
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/ComputedFields.lean b/src/Lean/Elab/ComputedFields.lean
index aadbd61075..15282017a6 100644
--- a/src/Lean/Elab/ComputedFields.lean
+++ b/src/Lean/Elab/ComputedFields.lean
@@ -186,8 +186,9 @@ def overrideComputedFields : M Unit := do
                 ← getComputedFieldValue cfn (mkAppN (mkConst ctor lparams) (params ++ fields))
             else
               mkLambdaFVars (compFieldVars ++ fields) cf
+    let cfnOverride := cfn ++ `_override
     addDecl <| .defnDecl {
-      name := cfn ++ `_override
+      name := cfnOverride
       levelParams
       type := ← mkForallFVars (params ++ indices ++ #[val]) (← inferType cf)
       value := ← mkLambdaFVars (params ++ indices ++ #[val]) <|
@@ -197,7 +198,9 @@ def overrideComputedFields : M Unit := do
       safety := .unsafe
       hints := .opaque
     }
-    setImplementedBy cfn (cfn ++ `_override)
+    if let some inlineAttr := Compiler.getInlineAttribute? (← getEnv) cfn then
+      setInlineAttribute cfnOverride inlineAttr
+    setImplementedBy cfn cfnOverride
 
 def mkComputedFieldOverrides (declName : Name) (compFields : Array Name) : MetaM Unit := do
   let ind ← getConstInfoInduct declName
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..6c6b3bee8f 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// update thy
+
 namespace lean {
 options get_default_options() {
     options opts;