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

refactor: split noncomputable error into its own helper (#9314)

Browse source
This commit is contained in:
Cameron Zwarich 2025-07-11 10:30:22 -07:00 • committed by GitHub
parent d4e11f754a
commit e2e36087e1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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