From cf14178929bb6761b4a4e21b76c8a1e67b6387bf Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sun, 29 Sep 2024 21:02:24 -0700
Subject: [PATCH] fix: default values for structure fields can be noncomputable
 (#5531)

Closes #2710
---
 src/Lean/Elab/Structure.lean | 3 ++-
 tests/lean/run/2710.lean     | 8 ++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/2710.lean

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 320aa17bd62c..1886fa132fbb 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -733,7 +733,8 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
         throwError "invalid default value for field, it contains metavariables{indentExpr value}"
       /- The identity function is used as "marker". -/
       let value ← mkId value
-      discard <| mkAuxDefinition declName type value (zetaDelta := true)
+      -- No need to compile the definition, since it is only used during elaboration.
+      discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
       setReducibleAttribute declName
 
 /--
diff --git a/tests/lean/run/2710.lean b/tests/lean/run/2710.lean
new file mode 100644
index 000000000000..7ed23b7e3cad
--- /dev/null
+++ b/tests/lean/run/2710.lean
@@ -0,0 +1,8 @@
+/-!
+# Structure field default values can be noncomputable
+-/
+
+noncomputable def ohno := 1
+
+structure OhNo where
+  x := ohno