Documentation

Lean.Compiler.LCNF.ReduceJpArity

Join point arity reduction.

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.ReduceJpArity.ReduceM (α : Type) :
Type
Equations
Instances For
    source
    partial def Lean.Compiler.LCNF.ReduceJpArity.reduce (code : Code Purity.pure) :
    ReduceM (Code Purity.pure)
    source
    def Lean.Compiler.LCNF.Decl.reduceJpArity (decl : Decl Purity.pure) :
    CompilerM (Decl Purity.pure)

    Try to reduce arity of join points

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Compiler.LCNF.reduceJpArity (phase : Phase := Phase.base) :
      Pass
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For