From e2e36087e1ff1c29043ded4949862d5da7a8cf4a Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Fri, 11 Jul 2025 10:30:22 -0700 Subject: [PATCH] refactor: split noncomputable error into its own helper (#9314) --- src/Lean/Compiler/LCNF/ToMono.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean index fe2a31b052..1f359b050b 100644 --- a/src/Lean/Compiler/LCNF/ToMono.lean +++ b/src/Lean/Compiler/LCNF/ToMono.lean @@ -23,9 +23,12 @@ def Param.toMono (param : Param) : ToMonoM Param := do modify fun s => { s with typeParams := s.typeParams.insert param.fvarId } param.update (← toMonoType param.type) +def throwNoncomputableError {α : Type} (declName : Name) : ToMonoM α := + throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName declName}', which is 'noncomputable'" + def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do if let some declName := (← get).noncomputableVars.get? fvarId then - throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName declName}', which is 'noncomputable'" + throwNoncomputableError declName def checkFVarUseDeferred (resultFVar fvarId : FVarId) : ToMonoM Unit := do if let some declName := (← get).noncomputableVars.get? fvarId then