Documentation

Lake.Config.LeanLibConfig

structure Lake.LeanLibConfig (name : Lean.Name) extends Lake.LeanConfig :

A Lean library's declarative configuration.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    @[reducible, inline]

    The library's name.

    Equations
    Instances For

      Whether the given module is considered local to the library.

      Equations
      Instances For

        Whether the given module is a buildable part of the library.

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