Documentation

Lean.Compiler.LCNF.ToDecl

source
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.
source
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.
source
partial def Lean.Compiler.LCNF.inlineMatchers.inlineMatcher (declName : Lean.Name) (us : List Lean.Level) (info : Lean.Meta.MatcherInfo) (numAlts : Nat) (altNumParams : Array Nat) (i : Nat) (args : Array Lean.Expr) (letFVars : Array Lean.Expr) :
Lean.MetaM Lean.Expr
source
def Lean.Compiler.LCNF.getDeclInfo? (declName : Lean.Name) :
Lean.CoreM (Option Lean.ConstantInfo)

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.
source
def Lean.Compiler.LCNF.toDecl (declName : Lean.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.