Documentation

Lean.Compiler.IR.ElimDeadVars

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

Equations

Lean.IR.reshapeWithoutDead bs term = (fun reshape => reshape bs term (Lean.IR.FnBody.freeIndices term)) Lean.IR.reshapeWithoutDead.reshape

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) :

Equations

Lean.IR.Decl.elimDead d = match d with | Lean.IR.Decl.fdecl x x_1 x_2 b x_3 => Lean.IR.Decl.updateBody! d (Lean.IR.FnBody.elimDead b) | other => other