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

• d.elimDead = match d with | Lean.IR.Decl.fdecl f xs type b info => d.updateBody! b.elimDead | other => other