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

fix: process remaining params

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-18 15:29:41 -07:00
parent 90b9b0b7e9
commit 5fbe63cca4
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Compiler/LCNF/Specialize.lean
View file

@ -307,6 +307,9 @@ where
-- Keep the parameter
let param := { param with type := param.type.instantiateLevelParams decl.levelParams us }
params := params.push (← internalizeParam param)
for param in decl.params[argMask.size:] do
let param := { param with type := param.type.instantiateLevelParams decl.levelParams us }
params := params.push (← internalizeParam param)
let value := decl.instantiateValueLevelParams us
let value ← internalizeCode value
let value := attachCodeDecls decls value