@[reducible, inline]

abbrev Lake.ExternLib : Type

An external library -- its package plus its configuration.

@[inline]

def Lake.Package.externLibs (self : Package) : Array ExternLib

The external libraries of the package (as an Array).

@[inline]

def Lake.Package.findExternLib? (name : Lean.Name) (self : Package) : Option ExternLib

Try to find a external library in the package with the given name.

@[inline]

def Lake.ExternLib.config (self : ExternLib) : ExternLibConfig self.pkg.name self.name

The library's user-defined configuration.

@[inline]

def Lake.ExternLib.linkArgs (self : ExternLib) : Array String

The arguments to pass to leanc when linking the external library. That is, the package's moreLinkArgs.

@[inline]

def Lake.ExternLib.staticTargetName (self : ExternLib) : Lean.Name

The name of the package target used to build the external library's static binary.