def Lean.Compiler.LCNF.macroInline (e : Expr) : CoreM Expr

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

def Lean.Compiler.LCNF.inlineMatchers (e : Expr) : CoreM Expr

Inline auxiliary matcher applications.

def Lean.Compiler.LCNF.getDeclInfo? (declName : Name) : CoreM (Option ConstantInfo)

Return the declaration ConstantInfo for the code generator.

Remark: the unsafe recursive version is tried first.

def Lean.Compiler.LCNF.declIsNotUnsafe (declName : Name) : CoreM Bool

def Lean.Compiler.LCNF.toDecl (declName : Name) : CompilerM Decl

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