Documentation

Lake.Config.ExternLibConfig

source
structure Lake.ExternLibConfig (pkgName name : Lean.Name) :
Type

A external library's declarative configuration.

Instances For
    source
    def Lake.instInhabitedExternLibConfig.default {a✝ a✝¹ : Lean.Name} :
    ExternLibConfig a✝ a✝¹
    Instances For
      source
      @[implicit_reducible]
      instance Lake.instInhabitedExternLibConfig {a✝ a✝¹ : Lean.Name} :
      Inhabited (ExternLibConfig a✝ a✝¹)