# Documentation

Lean.Compiler.LCNF.ToDecl

Inline constants tagged with the [macro_inline] attribute occurring in e.

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

Inline auxiliary matcher applications.

Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Compiler.LCNF.inlineMatchers.inlineMatcher (declName : Lean.Name) (us : ) (info : Lean.Meta.MatcherInfo) (numAlts : Nat) (altNumParams : ) (i : Nat) (args : ) (letFVars : ) :

Return the declaration ConstantInfo for the code generator.

Remark: the unsafe recursive version is tried first.

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

Convert the given declaration from the Lean environment into Decl. The steps for this are roughly:

• partially erasing type information of the declaration
• eta-expanding the declaration value.
• if the declaration has an unsafe-rec version, use it.
• expand declarations tagged with the [macro_inline] attribute
• turn the resulting term into LCNF declaration
Equations
• One or more equations did not get rendered due to their size.