Documentation

Lean.Compiler.IR.ElimDeadVars

def Lean.IR.reshapeWithoutDead (bs : Array Lean.IR.FnBody) (term : 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) :

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

def Lean.IR.Decl.elimDead (d : 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