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

Instances For

    Inline auxiliary matcher applications.

    Instances For
      partial def Lean.Compiler.LCNF.inlineMatchers.inlineMatcher (declName : Lake.Name) (us : List Lean.Level) (info : Lean.Meta.MatcherInfo) (numAlts : Nat) (altNumParams : Array Nat) (i : Nat) (args : Array Lean.Expr) (letFVars : Array Lean.Expr) :

      Return the declaration ConstantInfo for the code generator.

      Remark: the unsafe recursive version is tried first.

      Instances For

        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
        Instances For