Skip to content

Commit 0b2884b

Browse files
authored
fix: erase code of an erased type in LCNF simp (#8712)
This PR optimizes let decls of an erased type to an erased value. Specialization can create local functions that produce a Prop, and there's no point in keeping them around.
1 parent c53ab28 commit 0b2884b

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/Lean/Compiler/LCNF/Simp/Main.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -224,6 +224,9 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
224224
let mut decl ← normLetDecl baseDecl
225225
if baseDecl != decl then
226226
markSimplified
227+
if decl.type.isErased && decl.value != .erased then
228+
markSimplified
229+
decl ← decl.updateValue .erased
227230
if let some value ← simpValue? decl.value then
228231
markSimplified
229232
decl ← decl.updateValue value

0 commit comments

Comments
 (0)