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 : Lean.Compiler.LCNF.Code) :
    Lean.Compiler.LCNF.ReduceJpArity.ReduceM Lean.Compiler.LCNF.Code
    source
    def Lean.Compiler.LCNF.Decl.reduceJpArity (decl : Lean.Compiler.LCNF.Decl) :
    Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.Phase := Lean.Compiler.LCNF.Phase.base) :
      Lean.Compiler.LCNF.Pass
      Equations
      Instances For