@[reducible]

def Lake.Package.keyword : Lean.Name

The keyword for package declarations.

Equations

• Lake.Package.keyword = `package

@[reducible, match_pattern, inline]

abbrev Lake.Package.facetKind : Lean.Name

The kind identifier for facets of a package.

Equations

• Lake.Package.facetKind = Lake.Package.keyword

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

• Lake.Module.keyword = `module

@[reducible, match_pattern, inline]

abbrev Lake.Module.facetKind : Lean.Name

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

Equations

• Lake.Module.facetKind = Lake.Module.keyword

@[reducible]

def Lake.LeanLib.keyword : Lean.Name

The keyword for Lean library declarations.

Equations

• Lake.LeanLib.keyword = `lean_lib

@[reducible, match_pattern, inline]

abbrev Lake.LeanLib.facetKind : Lean.Name

The kind identifier for facets of a Lean library.

Equations

• Lake.LeanLib.facetKind = `lean_lib

@[reducible, match_pattern, inline]

abbrev Lake.LeanLib.configKind : Lean.Name

The type kind for Lean library configurations.

Equations

• Lake.LeanLib.configKind = Lake.LeanLib.facetKind

@[reducible]

def Lake.LeanExe.keyword : Lean.Name

The keyword for Lean executable declarations.

Equations

• Lake.LeanExe.keyword = `lean_exe

@[reducible, match_pattern, inline]

abbrev Lake.LeanExe.facetKind : Lean.Name

The kind identifier for facets of a Lean executable.

Equations

• Lake.LeanExe.facetKind = Lake.LeanExe.keyword

@[reducible, match_pattern, inline]

abbrev Lake.LeanExe.configKind : Lean.Name

The type kind for Lean executable configurations.

Equations

• Lake.LeanExe.configKind = Lake.LeanExe.facetKind

@[reducible]

def Lake.ExternLib.keyword : Lean.Name

The keyword for external library declarations.

Equations

• Lake.ExternLib.keyword = `extern_lib

@[reducible, match_pattern, inline]

abbrev Lake.ExternLib.facetKind : Lean.Name

The kind identifier for facets of an external library.

Equations

• Lake.ExternLib.facetKind = Lake.ExternLib.keyword

@[reducible, match_pattern, inline]

abbrev Lake.ExternLib.configKind : Lean.Name

The type kind for external library configurations.

Equations

• Lake.ExternLib.configKind = Lake.ExternLib.facetKind

@[reducible]

def Lake.InputFile.keyword : Lean.Name

The keyword for input file declarations.

Equations

• Lake.InputFile.keyword = `input_file

@[reducible, match_pattern, inline]

abbrev Lake.InputFile.facetKind : Lean.Name

The kind identifier for facets of an input file.

Equations

• Lake.InputFile.facetKind = Lake.InputFile.keyword

@[reducible, match_pattern, inline]

abbrev Lake.InputFile.configKind : Lean.Name

The type kind for input file configurations.

Equations

• Lake.InputFile.configKind = Lake.InputFile.facetKind

@[reducible]

def Lake.InputDir.keyword : Lean.Name

The keyword for input directory declarations.

Equations

• Lake.InputDir.keyword = `input_dir

@[reducible, match_pattern, inline]

abbrev Lake.InputDir.facetKind : Lean.Name

Tge kind identifier for facets of an input directory.

Equations

• Lake.InputDir.facetKind = Lake.InputDir.keyword

@[reducible, match_pattern, inline]

abbrev Lake.InputDir.configKind : Lean.Name

The type kind for input directory configurations.

Equations

• Lake.InputDir.configKind = Lake.InputDir.facetKind

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

• Lake.facetKindForNamespace `Lake.Package = Lake.Package.facetKind
• Lake.facetKindForNamespace `Lake.Module = Lake.Module.facetKind
• Lake.facetKindForNamespace `Lake.LeanLib = Lake.LeanLib.facetKind
• Lake.facetKindForNamespace `Lake.LeanExe = Lake.LeanExe.facetKind
• Lake.facetKindForNamespace `Lake.ExternLib = Lake.ExternLib.facetKind
• Lake.facetKindForNamespace `Lake.InputFile = Lake.InputFile.facetKind
• Lake.facetKindForNamespace `Lake.InputDir = Lake.InputDir.facetKind
• Lake.facetKindForNamespace ns = Lean.Name.anonymous