Documentation

Lean.Compiler.LCNF.ToDecl

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

Equations
    Instances For

      Inline auxiliary matcher applications.

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

          Return the declaration ConstantInfo for the code generator.

          Remark: the unsafe recursive version is tried first.

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