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

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

Equations

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

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

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 : Lake.Name) (us : List Lean.Level) (info : Lean.Meta.MatcherInfo) (i : Nat) (args : Array Lean.Expr) (letFVars : Array Lean.Expr) : Lean.MetaM Lean.Expr

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

Return the declaration ConstantInfo for the code generator.

Remark: the unsafe recursive version is tried first.

Equations

• Lean.Compiler.LCNF.getDeclInfo? declName = do let env ← Lean.getEnv pure (HOrElse.hOrElse (env.find? (Lean.Compiler.mkUnsafeRecName declName)) fun (x : Unit) => env.find? declName)

def Lean.Compiler.LCNF.toDecl (declName : Lake.Name) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.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

Equations

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