Join point arity reduction.

@[inline, reducible]

abbrev Lean.Compiler.LCNF.ReduceJpArity.ReduceM (α : Type) : Type

Equations

• Lean.Compiler.LCNF.ReduceJpArity.ReduceM = ReaderT (Lean.FVarIdMap (Array Bool)) Lean.Compiler.LCNF.CompilerM

partial def Lean.Compiler.LCNF.ReduceJpArity.reduce (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.ReduceJpArity.ReduceM Lean.Compiler.LCNF.Code

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.

def Lean.Compiler.LCNF.reduceJpArity (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) : Lean.Compiler.LCNF.Pass

Equations

• Lean.Compiler.LCNF.reduceJpArity phase = Lean.Compiler.LCNF.Pass.mkPerDeclaration `reduceJpArity Lean.Compiler.LCNF.Decl.reduceJpArity phase