partial def Lean.Compiler.LCNF.toMonoType (type : Lean.Expr) : Lean.Compiler.LCNF.CompilerM Lean.Expr

Convert a LCNF type from the base phase to the mono phase.

LCNF types in the mono phase do not have dependencies, and universe levels have been erased.

The type contains only → and constants.

partial def Lean.Compiler.LCNF.toMonoType.visitApp (f : Lean.Expr) (args : Array Lean.Expr) : Lean.Compiler.LCNF.CompilerM Lean.Expr