← Mathematical handbook

def Lean.Compiler.LCNF.lowerResultType (type : Expr) (arity : Nat) : CoreM Expr

Equations

• Lean.Compiler.LCNF.lowerResultType type arity = Lean.Compiler.LCNF.toImpureType (Lean.Compiler.LCNF.lowerResultType.resultTypeForArity✝ type arity)

def Lean.Compiler.LCNF.toImpure : Pass

Equations

• One or more equations did not get rendered due to their size.