def Lean.Compiler.LCNF.ToLCNF.toLCNF (e eType : Expr) : CompilerM (Code Purity.pure)

Put the given expression in LCNF.

• Nested proofs are replaced with lcProof-applications.
• Eta-expand applications of declarations that satisfy shouldEtaExpand.
• Put computationally relevant expressions in A-normal form.