Documentation

Lean.Compiler.LCNF.ToDecl

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

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

    Inline auxiliary matcher applications.

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

      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
        • One or more equations did not get rendered due to their size.
        Instances For