A dynamic/shared library artifact for linking.
- path : System.FilePath
Library file path.
- name : String
Library name without platform-specific prefix/suffix (for
-l
). - plugin : Bool
Whether this library can be loaded as a plugin.
Transitive dependencies of this library for situations that need them (e.g., linking on Windows, loading via
lean
).
Instances For
Equations
- Lake.instReprDynlib = { reprPrec := Lake.reprDynlib✝ }
Optional library directory (for -L
).
Instances For
Equations
- Lake.instToTextDynlib = { toText := fun (x : Lake.Dynlib) => x.path.toString }
Equations
- Lake.instToJsonDynlib = { toJson := fun (x : Lake.Dynlib) => Lean.Json.str x.path.toString }
Equations
- Lake.instCoeDynlibFilePath = { coe := fun (x : Lake.Dynlib) => x.path }