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) :
    ReduceM Code
    source
    def Lean.Compiler.LCNF.Decl.reduceJpArity (decl : Decl) :
    CompilerM Decl

    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
      Instances For