Documentation

Lake.Config.Kinds

source
@[reducible]
def Lake.Package.keyword :
Lean.Name

The keyword for package declarations.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.Package.facetKind :
Lean.Name

The kind identifier for facets of a package.

Equations
source
@[reducible]
def Lake.Module.keyword :
Lean.Name

The would-be keyword for module declarations.

Such declarations do not currently exist, but this is used as the facet kind for modules.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.Module.facetKind :
Lean.Name

The kind identifier for facets of a (Lean) module.

Equations
source
@[reducible]
def Lake.LeanLib.keyword :
Lean.Name

The keyword for Lean library declarations.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.LeanLib.facetKind :
Lean.Name

The kind identifier for facets of a Lean library.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.LeanLib.configKind :
Lean.Name

The type kind for Lean library configurations.

Equations
source
@[reducible]
def Lake.LeanExe.keyword :
Lean.Name

The keyword for Lean executable declarations.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.LeanExe.facetKind :
Lean.Name

The kind identifier for facets of a Lean executable.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.LeanExe.configKind :
Lean.Name

The type kind for Lean executable configurations.

Equations
source
@[reducible]
def Lake.ExternLib.keyword :
Lean.Name

The keyword for external library declarations.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.ExternLib.facetKind :
Lean.Name

The kind identifier for facets of an external library.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.ExternLib.configKind :
Lean.Name

The type kind for external library configurations.

Equations
source
@[reducible]
def Lake.InputFile.keyword :
Lean.Name

The keyword for input file declarations.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.InputFile.facetKind :
Lean.Name

The kind identifier for facets of an input file.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.InputFile.configKind :
Lean.Name

The type kind for input file configurations.

Equations
source
@[reducible]
def Lake.InputDir.keyword :
Lean.Name

The keyword for input directory declarations.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.InputDir.facetKind :
Lean.Name

Tge kind identifier for facets of an input directory.

Equations
source
@[reducible, match_pattern, inline]
abbrev Lake.InputDir.configKind :
Lean.Name

The type kind for input directory configurations.

Equations
source
def Lake.facetKindForNamespace (ns : Lean.Name) :
Lean.Name

Lake Internal. Returns the facet kind for an Lake target namespace. Used by the builtin_facet macro.

Equations