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

chore: propagate recursive flag during code specialization

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-30 20:01:18 -07:00
parent 9fda3d973d
commit 18b5ff9e78
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -327,7 +327,8 @@ where
let type ← value.inferType
let type ← mkForallParams params type
let safe := decl.safe
let decl := { name := nameNew, levelParams := levelParamsNew, params, type, value, safe : Decl }
let recursive := decl.recursive
let decl := { name := nameNew, levelParams := levelParamsNew, params, type, value, safe, recursive : Decl }
return decl.setLevelParams
/--