Documentation

Lake.Config.LeanLibConfig

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

A Lean library's declarative configuration.

Instances For
    instance Lake.LeanLibConfig.instConfigMeta :
    ConfigInfo `Lake.LeanLibConfig
    Equations
      @[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
                Instances For