Build Data Subtypes #
The open type family which maps a Lake data kind to its associated type.
For example, LeanLib.facetKind
maps to LeanLib
.
It is an open type, meaning additional mappings can be add lazily
as needed (via data_type
).
Equations
Instances For
Equations
Equations
Instances For
The open type family which maps a Lake facet to its output type.
For example, a FilePath
for the module.olean
facet.
It is an open type, meaning additional mappings can be add lazily
as needed (via facet_data
).
The open type family which maps a Lake facet kind and name to its output type.
For example, a FilePath
for the module
olean
facet.
It is an open type, meaning additional mappings can be add lazily
as needed (via facet_data
).
Equations
Instances For
The open type family which maps a module facet's name to its output type.
For example, a FilePath
for the module olean
facet.
It is an open type, meaning additional mappings can be add lazily
as needed (via module_data
).
Equations
Instances For
The open type family which maps a package facet's name to output type.
For example, an Arrry Package
of direct dependencies for the deps
facet.
It is an open type, meaning additional mappings can be add lazily
as needed (via package_data
).
Equations
Instances For
The open type family which maps a Lean library facet's name to its output type.
For example, the FilePath
pf the generated static library for the static
facet.
It is an open type, meaning additional mappings can be add lazily
as needed (via library_data
).
Equations
Instances For
The open type family which maps a Lean library facet's name to its output type.
For example, the FilePath
pf the generated static library for the static
facet.
It is an open type, meaning additional mappings can be add lazily
as needed (via library_data
).
Equations
Instances For
The open type family which maps a custom package targetto its output type.
It is an open type, meaning additional mappings can be add lazily
as needed (via custom_data
).
Equations
Instances For
Build Data #
A mapping between a build key and its associated build data in the store. It is a simple type function composed of the separate open type families for modules facets, package facets, Lake target facets, and custom targets.
Equations
Instances For
Macros for Declaring Build Data #
Macro for declaring new DatayType
.
Equations
Instances For
Internal macro for declaring new facet within Lake.