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

perf: during specialization, don't abstract all local fun decls under binders (#9596)

Browse source 
The `isUnderBinder` check is intended to avoid inlining repeated
computations into specializations, but this doesn’t apply to local
function decls whose bodies are already delayed.
This commit is contained in:
Cameron Zwarich 2025-07-28 10:36:43 -07:00 • committed by GitHub
parent 0fe7cc8794
commit 475bd65c90
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/Closure.lean
View file

@ -136,7 +136,7 @@ mutual
if ctx.inScope fvarId then
/- We only collect the variables in the scope of the function application being specialized. -/
if let some funDecl ← findFunDecl? fvarId then
if ctx.isUnderBinder || ctx.abstract funDecl.fvarId then
if ctx.abstract funDecl.fvarId then
modify fun s => { s with params := s.params.push <| { funDecl with borrow := false } }
else
collectFunDecl funDecl