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

A external library's declarative configuration.

• getJob : Lake.CustomData (pkgName, name.str "static") → Lake.BuildJob System.FilePath

  The library's build data.

instance Lake.instInhabitedExternLibConfig : {a a_1 : Lean.Name} → Inhabited (Lake.ExternLibConfig a a_1)

Equations

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

structure Lake.ExternLibDecl : Type

A dependently typed configuration based on its registered package and name.

• pkg : Lean.Name
• name : Lean.Name
• config : Lake.ExternLibConfig self.pkg self.name