def Lean.IR.reshapeWithoutDead (bs : Array Lean.IR.FnBody) (term : Lean.IR.FnBody) : Lean.IR.FnBody

Equations

• Lean.IR.reshapeWithoutDead bs term = Lean.IR.reshapeWithoutDead.reshape bs term term.freeIndices

partial def Lean.IR.reshapeWithoutDead.reshape (bs : Array Lean.IR.FnBody) (b : Lean.IR.FnBody) (used : Lean.IR.IndexSet) : Lean.IR.FnBody

partial def Lean.IR.FnBody.elimDead (b : Lean.IR.FnBody) : Lean.IR.FnBody

def Lean.IR.Decl.elimDead (d : Lean.IR.Decl) : Lean.IR.Decl

Eliminate dead let-declarations and join points

Equations

• (Lean.IR.Decl.fdecl f xs type b info).elimDead = (Lean.IR.Decl.fdecl f xs type b info).updateBody! b.elimDead
• d.elimDead = d