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 (Lean.IR.FnBody.freeIndices term)

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.elimDead d = match d with | Lean.IR.Decl.fdecl f xs type b info => Lean.IR.Decl.updateBody! d (Lean.IR.FnBody.elimDead b) | other => other