fix: default values for structure fields can be noncomputable (#5531)

Closes #2710
leanprover · Sep 30, 2024 · cf14178 · cf14178
1 parent a4dfa83
commit cf14178
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git 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
@@ -0,0 +1,8 @@
+/-!
+# Structure field default values can be noncomputable
+-/
+
+noncomputable def ohno := 1
+
+structure OhNo where
+  x := ohno