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.

Equations

• Lean.Compiler.LCNF.toLCNF e eType = Lean.Compiler.LCNF.ToLCNF.run✝ eType do let __do_lift ← Lean.Compiler.LCNF.ToLCNF.toLCNF.visit✝ e Lean.Compiler.LCNF.ToLCNF.toCode✝ __do_lift