@[reducible]

def Lake.Package.keyword : Lean.Name

The keyword for package declarations.

@[reducible, match_pattern, inline]

abbrev Lake.Package.facetKind : Lean.Name

The kind identifier for facets of a package.

@[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.

@[reducible, match_pattern, inline]

abbrev Lake.Module.facetKind : Lean.Name

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

@[reducible]

def Lake.LeanLib.keyword : Lean.Name

The keyword for Lean library declarations.

@[reducible, match_pattern, inline]

abbrev Lake.LeanLib.facetKind : Lean.Name

The kind identifier for facets of a Lean library.

@[reducible, match_pattern, inline]

abbrev Lake.LeanLib.configKind : Lean.Name

The type kind for Lean library configurations.

@[reducible]

def Lake.LeanExe.keyword : Lean.Name

The keyword for Lean executable declarations.

@[reducible, match_pattern, inline]

abbrev Lake.LeanExe.facetKind : Lean.Name

The kind identifier for facets of a Lean executable.

@[reducible, match_pattern, inline]

abbrev Lake.LeanExe.configKind : Lean.Name

The type kind for Lean executable configurations.

@[reducible]

def Lake.ExternLib.keyword : Lean.Name

The keyword for external library declarations.

@[reducible, match_pattern, inline]

abbrev Lake.ExternLib.facetKind : Lean.Name

The kind identifier for facets of an external library.

@[reducible, match_pattern, inline]

abbrev Lake.ExternLib.configKind : Lean.Name

The type kind for external library configurations.

@[reducible]

def Lake.InputFile.keyword : Lean.Name

The keyword for input file declarations.

@[reducible, match_pattern, inline]

abbrev Lake.InputFile.facetKind : Lean.Name

The kind identifier for facets of an input file.

@[reducible, match_pattern, inline]

abbrev Lake.InputFile.configKind : Lean.Name

The type kind for input file configurations.

@[reducible]

def Lake.InputDir.keyword : Lean.Name

The keyword for input directory declarations.

@[reducible, match_pattern, inline]

abbrev Lake.InputDir.facetKind : Lean.Name

The kind identifier for facets of an input directory.

@[reducible, match_pattern, inline]

abbrev Lake.InputDir.configKind : Lean.Name

The type kind for input directory configurations.

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.