feat: support extern computed fields

src/Lean/Elab/ComputedFields.lean

@@ -135,6 +135,9 @@ def overrideComputedFields : M Unit := do
   let {name, levelParams, ctors, compFields, compFieldVars, lparams, params, indices, val ..} ← read
   withLocalDeclD `x (mkAppN (mkConst (name ++ `_impl) lparams) (params ++ indices)) fun xImpl => do
   for cfn in compFields, cf in compFieldVars do
+    if isExtern (← getEnv) cfn then
+      compileDecls [cfn]
+      continue
     let cases ← ctors.toArray.mapM fun ctor => do
       forallTelescope (← inferType (mkAppN (mkConst ctor lparams) params)) fun fields _ => do
       if ← isScalarField ctor then
@@ -199,5 +202,6 @@ def setComputedFields (computedFields : Array (Name × Array Name)) : MetaM Unit
     for ctor in ind.ctors do
       toCompile := toCompile.push (ctor ++ `_override)
     for fieldName in computedFields do
-      toCompile := toCompile.push <| fieldName ++ `_override
+      unless isExtern (← getEnv) fieldName do
+        toCompile := toCompile.push <| fieldName ++ `_override
   compileDecls toCompile.toList

tests/compiler/computedFieldsExtern.lean

@@ -0,0 +1,12 @@
+inductive Exp
+  | var (i : Nat)
+  | app (a b : Exp)
+with
+  @[extern c inline "(lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*)) + 40)"]
+  hash : Exp → UInt64
+    | .var i => Hashable.hash i
+    | .app a b => a.hash + b.hash
+
+def main : IO Unit := do
+  -- should be 30 + 3*40 = 150
+  IO.println <| Exp.hash (.app (.var 10) (.var 20))

tests/compiler/computedFieldsExtern.lean.expected.out

@@ -0,0 +1 @@
+150