structure Lake.Dynlib : Type

A dynamic/shared library for linking.

• path : System.FilePath

  Library file path.

• name : String

  Library name without platform-specific prefix/suffix (for -l).

def Lake.Dynlib.dir? (self : Dynlib) : Option System.FilePath

Optional library directory (for -L).

Equations

• self.dir? = self.path.parent

instance Lake.instToTextDynlib : ToText Dynlib

Equations

• Lake.instToTextDynlib = { toText := fun (x : Lake.Dynlib) => x.path.toString }

instance Lake.instToJsonDynlib : Lean.ToJson Dynlib

Equations

• Lake.instToJsonDynlib = { toJson := fun (x : Lake.Dynlib) => Lean.Json.str x.path.toString }