diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 320aa17bd6..1886fa132f 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 0000000000..7ed23b7e3c --- /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