Documentation

Lean.Compiler.LCNF.ElimDead

This module implements a pass that does a syntactic use-def check for all let/fun/jp bindings and removes them if they are unused. Note that in impure mode not all unused let bindings can be removed safely so we opt for a safe subset.

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.UsedLocalDecls :
Type
Equations
Instances For
    source
    def Lean.Compiler.LCNF.Decl.elimDeadVars {pu : Purity} (decl : Decl pu) :
    CompilerM (Decl pu)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Compiler.LCNF.elimDeadVars (phase : Phase) (occurrence : Nat) :
      Pass
      Equations
      Instances For