From bd06e076241c5f8d29706edcd38d8bd924533d0c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 5 Jul 2025 22:28:35 +0100 Subject: [PATCH] fix: make the name in dependsOnNoncomputable clickable (#9207) This PR makes the offending declaration clickable in the error message produced when something should be marked `noncomputable`. --- src/Lean/Compiler/LCNF/ToMono.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean index 1fb1636ee4..42ca5f7c57 100644 --- a/src/Lean/Compiler/LCNF/ToMono.lean +++ b/src/Lean/Compiler/LCNF/ToMono.lean @@ -30,7 +30,7 @@ def isTrivialConstructorApp? (declName : Name) (args : Array Arg) : ToMonoM (Opt def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do if let some declName := (← get).noncomputableVars.get? fvarId then - throwNamedError lean.dependsOnNoncomputable f!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{declName}', which is 'noncomputable'" + throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName declName}', which is 'noncomputable'" def checkFVarUseDeferred (resultFVar fvarId : FVarId) : ToMonoM Unit := do if let some declName := (← get).noncomputableVars.get? fvarId then