Simple Builtin Facet Declarations

This module contains the definitions of most of the builtin facets. The others are defined Build.Info. The facets there require configuration definitions (e.g., Module), and some of the facets here are used in said definitions.

Module Facets

structure Lake.ModuleFacet (α : Type) : Type

A module facet name along with proof of its data type.

• name : Lean.Name

  The name of the module facet.

• data_eq : FacetOut self.name = α

  Proof that module's facet build result is of type α.

def Lake.instReprModuleFacet.repr {α✝ : Type} [Repr α✝] : ModuleFacet α✝ → Nat → Std.Format

instance Lake.instReprModuleFacet {α✝ : Type} [Repr α✝] : Repr (ModuleFacet α✝)

instance Lake.instFamilyDefNameFacetOutName {α : Type} (facet : ModuleFacet α) : FamilyDef FacetOut facet.name α

instance Lake.instCoeDepNameModuleFacetOfFamilyOutFacetOut {facet : Lean.Name} {α : Type} [FamilyOut FacetOut facet α] : CoeDep Lean.Name facet (ModuleFacet α)

@[simp]

axiom Lake.FacetOut.module.lean : FacetOut `module.lean = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath : FamilyDef FacetOut (`module ++ `lean) System.FilePath

@[reducible]

def Lake.Module.leanFacet : Lean.Name

The module's Lean source file.

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath : FamilyDef FacetOut `module.lean System.FilePath

@[reducible]

def Lake.Module.headerFacet : Lean.Name

The parsed module header of the module's source file.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleHeader : FamilyDef FacetOut (`module ++ `header) Lean.ModuleHeader

@[simp]

axiom Lake.FacetOut.module.header : FacetOut `module.header = Lean.ModuleHeader

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleHeader : FamilyDef FacetOut `module.header Lean.ModuleHeader

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleSetup : FamilyDef FacetOut (`module ++ `setup) Lean.ModuleSetup

@[simp]

axiom Lake.FacetOut.module.setup : FacetOut `module.setup = Lean.ModuleSetup

@[reducible]

def Lake.Module.setupFacet : Lean.Name

The computed configuration of a module for Lean.

In the process, this facet will build all of a module's dependencies, including transitive imports, plugins, and those specified by needs.

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleSetup : FamilyDef FacetOut `module.setup Lean.ModuleSetup

@[reducible]

def Lake.Module.depsFacet : Lean.Name

This facet builds all of a module's dependencies, including transitive imports, plugins, and those specified by needs.

instance Lake.instFamilyDefNameFacetOutMkStr2Opaque : FamilyDef FacetOut `module.deps Opaque

@[simp]

axiom Lake.FacetOut.module.deps : FacetOut `module.deps = Opaque

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Opaque : FamilyDef FacetOut (`module ++ `deps) Opaque

structure Lake.ModuleImportInfo : Type

Information about the imports of a module.

• directArts : Lean.NameMap Lean.ImportArtifacts

  Artifacts directly needed for the imports of the module.

• trace : BuildTrace

  The trace produced by mixing the traces of directArts with their transitive imports.

• transTrace : BuildTrace

  Transitive import trace for an import of the module with the module system enabled.

• metaTransTrace : BuildTrace

  Transitive import trace for a meta import of the module.

• allTransTrace : BuildTrace

  Transitive import trace for an import all of the module.

• legacyTransTrace : BuildTrace

  Transitive import trace for an import of the module without the module system enabled.

def Lake.instInhabitedModuleImportInfo.default : ModuleImportInfo

instance Lake.instInhabitedModuleImportInfo : Inhabited ModuleImportInfo

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleImportInfo : FamilyDef FacetOut `module.importInfo ModuleImportInfo

@[reducible]

def Lake.Module.importInfoFacet : Lean.Name

For internal use only. Information about the imports of this module.

@[simp]

axiom Lake.FacetOut.module.importInfo : FacetOut `module.importInfo = ModuleImportInfo

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleImportInfo : FamilyDef FacetOut (`module ++ `importInfo) ModuleImportInfo

structure Lake.ModuleExportInfo : Type

Information useful to importers of a module.

• srcTrace : BuildTrace

  The trace of the module's source file.

• arts : Lean.ImportArtifacts

  Artifacts directly needed for an import of the module with the module system enabled.

• artsTrace : BuildTrace

  The trace of the module's public olean.

• metaArtsTrace : BuildTrace

  The trace of the module's public olean and IR.

• allArts : Lean.ImportArtifacts

  Artifacts directly needed for an import of the module from a module without the module system enabled or import all of the module from a module with it enabled.

• allArtsTrace : BuildTrace

  The trace produced by mixing the traces of allArts.

• transTrace : BuildTrace

  Transitive import trace for an import of the module with the module system enabled.

• metaTransTrace : BuildTrace

  Transitive import trace for a meta import of the module.

• allTransTrace : BuildTrace

  Transitive import trace for an import all of the module.

• legacyTransTrace : BuildTrace

  Transitive import trace for an import of the module without the module system enabled.

def Lake.instInhabitedModuleExportInfo.default : ModuleExportInfo

instance Lake.instInhabitedModuleExportInfo : Inhabited ModuleExportInfo

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleExportInfo : FamilyDef FacetOut `module.exportInfo ModuleExportInfo

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleExportInfo : FamilyDef FacetOut (`module ++ `exportInfo) ModuleExportInfo

@[reducible]

def Lake.Module.exportInfoFacet : Lean.Name

For internal use only. Information useful to importers of this module.

@[simp]

axiom Lake.FacetOut.module.exportInfo : FacetOut `module.exportInfo = ModuleExportInfo

instance Lake.instFamilyDefNameFacetOutMkStr2ImportArtifacts : FamilyDef FacetOut `module.importArts Lean.ImportArtifacts

@[simp]

axiom Lake.FacetOut.module.importArts : FacetOut `module.importArts = Lean.ImportArtifacts

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ImportArtifacts : FamilyDef FacetOut (`module ++ `importArts) Lean.ImportArtifacts

@[reducible]

def Lake.Module.importArtsFacet : Lean.Name

Artifacts directly needed for an import of this module with the module system enabled.

instance Lake.instFamilyDefNameFacetOutMkStr2ImportArtifacts_1 : FamilyDef FacetOut `module.importAllArts Lean.ImportArtifacts

@[reducible]

def Lake.Module.importAllArtsFacet : Lean.Name

Artifacts directly needed for an import of this module from a module without the module system enabled or import all of this module from a module with it enabled.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ImportArtifacts_1 : FamilyDef FacetOut (`module ++ `importAllArts) Lean.ImportArtifacts

@[simp]

axiom Lake.FacetOut.module.importAllArts : FacetOut `module.importAllArts = Lean.ImportArtifacts

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleOutputArtifacts : FamilyDef FacetOut (`module ++ `leanArts) ModuleOutputArtifacts

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleOutputArtifacts : FamilyDef FacetOut `module.leanArts ModuleOutputArtifacts

@[reducible]

def Lake.Module.leanArtsFacet : Lean.Name

The core build facet of a Lean file. Elaborates the Lean file via lean and produces all the Lean artifacts of the module (e.g., olean, ilean, c). Its trace just includes its dependencies.

@[simp]

axiom Lake.FacetOut.module.leanArts : FacetOut `module.leanArts = ModuleOutputArtifacts

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_1 : FamilyDef FacetOut `module.olean System.FilePath

@[simp]

axiom Lake.FacetOut.module.olean : FacetOut `module.olean = System.FilePath

@[reducible]

def Lake.Module.oleanFacet : Lean.Name

The olean file produced by lean.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_1 : FamilyDef FacetOut (`module ++ `olean) System.FilePath

@[reducible]

def Lake.Module.oleanServerFacet : Lean.Name

The olean.server file produced by lean (with the module system enabled).

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath : FamilyDef FacetOut (`module ++ `olean.server) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath : FamilyDef FacetOut `module.olean.server System.FilePath

@[simp]

axiom Lake.FacetOut.module.olean.server : FacetOut `module.olean.server = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_1 : FamilyDef FacetOut `module.olean.private System.FilePath

@[simp]

axiom Lake.FacetOut.module.olean.private : FacetOut `module.olean.private = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_1 : FamilyDef FacetOut (`module ++ `olean.private) System.FilePath

@[reducible]

def Lake.Module.oleanPrivateFacet : Lean.Name

The olean.private file produced by lean (with the module system enabled).

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_2 : FamilyDef FacetOut `module.ilean System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_2 : FamilyDef FacetOut (`module ++ `ilean) System.FilePath

@[simp]

axiom Lake.FacetOut.module.ilean : FacetOut `module.ilean = System.FilePath

@[reducible]

def Lake.Module.ileanFacet : Lean.Name

The ilean file produced by lean.

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_3 : FamilyDef FacetOut `module.ir System.FilePath

@[simp]

axiom Lake.FacetOut.module.ir : FacetOut `module.ir = System.FilePath

@[reducible]

def Lake.Module.irFacet : Lean.Name

The ir file produced by lean (with the module system enabled).

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_3 : FamilyDef FacetOut (`module ++ `ir) System.FilePath

@[simp]

axiom Lake.FacetOut.module.c : FacetOut `module.c = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_4 : FamilyDef FacetOut (`module ++ `c) System.FilePath

@[reducible]

def Lake.Module.cFacet : Lean.Name

The C file produced by lean.

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_4 : FamilyDef FacetOut `module.c System.FilePath

@[reducible]

def Lake.Module.bcFacet : Lean.Name

The LLVM bitcode (bc) file produced by lean.

@[simp]

axiom Lake.FacetOut.module.bc : FacetOut `module.bc = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_5 : FamilyDef FacetOut (`module ++ `bc) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_5 : FamilyDef FacetOut `module.bc System.FilePath

@[simp]

axiom Lake.FacetOut.module.c.o : FacetOut `module.c.o = System.FilePath

@[reducible]

def Lake.Module.coFacet : Lean.Name

The object file .c.o built from c. On Windows, this is c.o.noexport, on other systems it is c.o.export).

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_2 : FamilyDef FacetOut `module.c.o System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_2 : FamilyDef FacetOut (`module ++ `c.o) System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath : FamilyDef FacetOut (`module ++ `c.o.export) System.FilePath

@[simp]

axiom Lake.FacetOut.module.c.o.export : FacetOut `module.c.o.export = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr4FilePath : FamilyDef FacetOut `module.c.o.export System.FilePath

@[reducible]

def Lake.Module.coExportFacet : Lean.Name

The object file .c.o.export built from c (with -DLEAN_EXPORTING).

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath_1 : FamilyDef FacetOut (`module ++ `c.o.noexport) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr4FilePath_1 : FamilyDef FacetOut `module.c.o.noexport System.FilePath

@[simp]

axiom Lake.FacetOut.module.c.o.noexport : FacetOut `module.c.o.noexport = System.FilePath

@[reducible]

def Lake.Module.coNoExportFacet : Lean.Name

The object file .c.o.noexport built from c (without -DLEAN_EXPORTING).

@[reducible]

def Lake.Module.bcoFacet : Lean.Name

The object file .bc.o built from bc.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_3 : FamilyDef FacetOut (`module ++ `bc.o) System.FilePath

@[simp]

axiom Lake.FacetOut.module.bc.o : FacetOut `module.bc.o = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_3 : FamilyDef FacetOut `module.bc.o System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_6 : FamilyDef FacetOut (`module ++ `o) System.FilePath

@[simp]

axiom Lake.FacetOut.module.o : FacetOut `module.o = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_6 : FamilyDef FacetOut `module.o System.FilePath

@[reducible]

def Lake.Module.oFacet : Lean.Name

The object file built from c/bc. On Windows with the C backend, no Lean symbols are exported. On every other configuration, symbols are exported.

@[simp]

axiom Lake.FacetOut.module.o.export : FacetOut `module.o.export = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_4 : FamilyDef FacetOut (`module ++ `o.export) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_4 : FamilyDef FacetOut `module.o.export System.FilePath

@[reducible]

def Lake.Module.oExportFacet : Lean.Name

The object file built from c/bc (with Lean symbols exported).

@[simp]

axiom Lake.FacetOut.module.o.noexport : FacetOut `module.o.noexport = System.FilePath

@[reducible]

def Lake.Module.oNoExportFacet : Lean.Name

The object file built from c/bc (without Lean symbols exported).

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_5 : FamilyDef FacetOut (`module ++ `o.noexport) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_5 : FamilyDef FacetOut `module.o.noexport System.FilePath

Package Facets

@[reducible]

def Lake.Package.optBuildCacheFacet : Lean.Name

A package's optional cached build archive (e.g., from Reservoir or GitHub). Will NOT cause the whole build to fail if the archive cannot be fetched.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool : FamilyDef FacetOut (`package ++ `optCache) Bool

@[simp]

axiom Lake.FacetOut.package.optCache : FacetOut `package.optCache = Bool

instance Lake.instFamilyDefNameFacetOutMkStr2Bool : FamilyDef FacetOut `package.optCache Bool

@[simp]

axiom Lake.FacetOut.package.cache : FacetOut `package.cache = Unit

instance Lake.instFamilyDefNameFacetOutMkStr2Unit : FamilyDef FacetOut `package.cache Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit : FamilyDef FacetOut (`package ++ `cache) Unit

@[reducible]

def Lake.Package.buildCacheFacet : Lean.Name

A package's cached build archive (e.g., from Reservoir or GitHub). Will cause the whole build to fail if the archive cannot be fetched.

@[simp]

axiom Lake.FacetOut.package.optBarrel : FacetOut `package.optBarrel = Bool

@[reducible]

def Lake.Package.optReservoirBarrelFacet : Lean.Name

A package's optional build archive from Reservoir. Will NOT cause the whole build to fail if the barrel cannot be fetched.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool_1 : FamilyDef FacetOut (`package ++ `optBarrel) Bool

instance Lake.instFamilyDefNameFacetOutMkStr2Bool_1 : FamilyDef FacetOut `package.optBarrel Bool

@[simp]

axiom Lake.FacetOut.package.barrel : FacetOut `package.barrel = Unit

@[reducible]

def Lake.Package.reservoirBarrelFacet : Lean.Name

A package's Reservoir build archive from Reservoir. Will cause the whole build to fail if the barrel cannot be fetched.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_1 : FamilyDef FacetOut (`package ++ `barrel) Unit

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_1 : FamilyDef FacetOut `package.barrel Unit

@[reducible]

def Lake.Package.optGitHubReleaseFacet : Lean.Name

A package's optional build archive from a GitHub release. Will NOT cause the whole build to fail if the release cannot be fetched.

@[simp]

axiom Lake.FacetOut.package.optRelease : FacetOut `package.optRelease = Bool

instance Lake.instFamilyDefNameFacetOutMkStr2Bool_2 : FamilyDef FacetOut `package.optRelease Bool

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool_2 : FamilyDef FacetOut (`package ++ `optRelease) Bool

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_2 : FamilyDef FacetOut `package.release Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_2 : FamilyDef FacetOut (`package ++ `release) Unit

@[reducible]

def Lake.Package.gitHubReleaseFacet : Lean.Name

A package's build archive from a GitHub release. Will cause the whole build to fail if the release cannot be fetched.

@[simp]

axiom Lake.FacetOut.package.release : FacetOut `package.release = Unit

@[simp]

axiom Lake.FacetOut.package.extraDep : FacetOut `package.extraDep = Unit

@[reducible]

def Lake.Package.extraDepFacet : Lean.Name

A package's extraDepTargets mixed with its transitive dependencies'.

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_3 : FamilyDef FacetOut `package.extraDep Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_3 : FamilyDef FacetOut (`package ++ `extraDep) Unit

Target Facets

@[reducible]

def Lake.LeanLib.defaultFacet : Lean.Name

The library's default facets (as specified by its defaultFacets configuration). .

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_4 : FamilyDef FacetOut `lean_lib.default Unit

@[simp]

axiom Lake.FacetOut.lean_lib.default : FacetOut `lean_lib.default = Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_4 : FamilyDef FacetOut (`lean_lib ++ `default) Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_5 : FamilyDef FacetOut (`lean_lib ++ `leanArts) Unit

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_5 : FamilyDef FacetOut `lean_lib.leanArts Unit

@[simp]

axiom Lake.FacetOut.lean_lib.leanArts : FacetOut `lean_lib.leanArts = Unit

@[reducible]

def Lake.LeanLib.leanArtsFacet : Lean.Name

A Lean library's Lean artifacts (e.g., olean, ilean, c).

@[simp]

axiom Lake.FacetOut.lean_lib.static : FacetOut `lean_lib.static = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_7 : FamilyDef FacetOut (`lean_lib ++ `static) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_7 : FamilyDef FacetOut `lean_lib.static System.FilePath

@[reducible]

def Lake.LeanLib.staticFacet : Lean.Name

A Lean library's static artifact.

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_6 : FamilyDef FacetOut `lean_lib.static.export System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_6 : FamilyDef FacetOut (`lean_lib ++ `static.export) System.FilePath

@[reducible]

def Lake.LeanLib.staticExportFacet : Lean.Name

A Lean library's static artifact (with exported symbols).

Static libraries with explicit exports are built as thin libraries. Such libraries are usually used as part of the local build process of some shared artifact and not publicly distributed. Standard static libraries are much better for distribution.

@[simp]

axiom Lake.FacetOut.lean_lib.static.export : FacetOut `lean_lib.static.export = System.FilePath

@[simp]

axiom Lake.FacetOut.lean_lib.shared : FacetOut `lean_lib.shared = Dynlib

@[reducible]

def Lake.LeanLib.sharedFacet : Lean.Name

A Lean library's shared artifact.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Dynlib : FamilyDef FacetOut (`lean_lib ++ `shared) Dynlib

instance Lake.instFamilyDefNameFacetOutMkStr2Dynlib : FamilyDef FacetOut `lean_lib.shared Dynlib

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_6 : FamilyDef FacetOut (`lean_lib ++ `extraDep) Unit

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_6 : FamilyDef FacetOut `lean_lib.extraDep Unit

@[reducible]

def Lake.LeanLib.extraDepFacet : Lean.Name

A Lean library's extraDepTargets mixed with its package's.

@[simp]

axiom Lake.FacetOut.lean_lib.extraDep : FacetOut `lean_lib.extraDep = Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_8 : FamilyDef FacetOut (`lean_exe ++ `default) System.FilePath

@[simp]

axiom Lake.FacetOut.lean_exe.default : FacetOut `lean_exe.default = System.FilePath

@[reducible]

def Lake.LeanExe.defaultFacet : Lean.Name

The executable's default facet (i.e., an alias for exe)

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_8 : FamilyDef FacetOut `lean_exe.default System.FilePath

@[simp]

axiom Lake.FacetOut.lean_exe.exe : FacetOut `lean_exe.exe = System.FilePath

@[reducible]

def Lake.LeanExe.exeFacet : Lean.Name

A Lean binary executable.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_9 : FamilyDef FacetOut (`lean_exe ++ `exe) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_9 : FamilyDef FacetOut `lean_exe.exe System.FilePath

@[reducible]

def Lake.ExternLib.defaultFacet : Lean.Name

The external library's default facet (i.e., an alias for static)

@[simp]

axiom Lake.FacetOut.extern_lib.default : FacetOut `extern_lib.default = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_10 : FamilyDef FacetOut `extern_lib.default System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_10 : FamilyDef FacetOut (`extern_lib ++ `default) System.FilePath

@[simp]

axiom Lake.FacetOut.extern_lib.static : FacetOut `extern_lib.static = System.FilePath

@[reducible]

def Lake.ExternLib.staticFacet : Lean.Name

A external library's static binary.

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_11 : FamilyDef FacetOut `extern_lib.static System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_11 : FamilyDef FacetOut (`extern_lib ++ `static) System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_12 : FamilyDef FacetOut (`extern_lib ++ `shared) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_12 : FamilyDef FacetOut `extern_lib.shared System.FilePath

@[simp]

axiom Lake.FacetOut.extern_lib.shared : FacetOut `extern_lib.shared = System.FilePath

@[reducible]

def Lake.ExternLib.sharedFacet : Lean.Name

A external library's shared binary.

@[simp]

axiom Lake.FacetOut.extern_lib.dynlib : FacetOut `extern_lib.dynlib = Dynlib

@[reducible]

def Lake.ExternLib.dynlibFacet : Lean.Name

A external library's dynlib.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Dynlib_1 : FamilyDef FacetOut (`extern_lib ++ `dynlib) Dynlib

instance Lake.instFamilyDefNameFacetOutMkStr2Dynlib_1 : FamilyDef FacetOut `extern_lib.dynlib Dynlib

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_13 : FamilyDef FacetOut (`input_file ++ `default) System.FilePath

@[reducible]

def Lake.InputFile.defaultFacet : Lean.Name

The default facet for an input file. Produces the file path.

@[simp]

axiom Lake.FacetOut.input_file.default : FacetOut `input_file.default = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_13 : FamilyDef FacetOut `input_file.default System.FilePath

@[simp]

axiom Lake.FacetOut.input_dir.default : FacetOut `input_dir.default = Array System.FilePath

@[reducible]

def Lake.InputDir.defaultFacet : Lean.Name

The default facet for an input directory. Produces the matching files in the directory.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayFilePath : FamilyDef FacetOut (`input_dir ++ `default) (Array System.FilePath)

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayFilePath : FamilyDef FacetOut `input_dir.default (Array System.FilePath)