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

A external library's declarative configuration.

• getPath : Job (CustomData pkgName (name.str "static")) → Job System.FilePath

  The library's build data.

def Lake.instInhabitedExternLibConfig.default {a✝ a✝¹ : Lean.Name} : ExternLibConfig a✝ a✝¹

Equations

• Lake.instInhabitedExternLibConfig.default = { getPath := default }

instance Lake.instInhabitedExternLibConfig {a✝ a✝¹ : Lean.Name} : Inhabited (ExternLibConfig a✝ a✝¹)

Equations

• Lake.instInhabitedExternLibConfig = { default := Lake.instInhabitedExternLibConfig.default }