max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: make the name in dependsOnNoncomputable clickable (#9207)

Browse source 
This PR makes the offending declaration clickable in the error message
produced when something should be marked `noncomputable`.
This commit is contained in:
Eric Wieser 2025-07-05 22:28:35 +01:00 • committed by GitHub
parent 2cf6c2ddc9
commit bd06e07624
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/LCNF/ToMono.lean
View file

@ -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