# Module Setup Information #

Data types used by Lean module headers and the `--setup` CLI.

source
structure Lean.Import :
Type

- module : Name
- importAll : Bool

  `import all`; whether to import and expose all data saved by the module.

- isExported : Bool

  Whether to activate this import when the current module itself is imported.

- isMeta : Bool

  Whether to import IR for all definitions (transitively) reachable.

Instances For

source
def Lean.instReprImport.repr :
Import → Nat → Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instReprImport :
Repr Import
Equations

- Lean.instReprImport = { reprPrec := Lean.instReprImport.repr }

source
instance Lean.instInhabitedImport :
Inhabited Import
Equations

- Lean.instInhabitedImport = { default := Lean.instInhabitedImport.default }

source
def Lean.instInhabitedImport.default :
Import
Equations

- Lean.instInhabitedImport.default = { module := default, importAll := default, isExported := default, isMeta := default }

Instances For

source
def Lean.instToJsonImport.toJson :
Import → Json
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instToJsonImport :
ToJson Import
Equations

- Lean.instToJsonImport = { toJson := Lean.instToJsonImport.toJson }

source
def Lean.instFromJsonImport.fromJson :
Json → Except String Import
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instFromJsonImport :
FromJson Import
Equations

- Lean.instFromJsonImport = { fromJson? := Lean.instFromJsonImport.fromJson }

source
instance Lean.instBEqImport :
BEq Import
Equations

- Lean.instBEqImport = { beq := Lean.instBEqImport.beq }

source
def Lean.instBEqImport.beq :
Import → Import → Bool
Equations

- One or more equations did not get rendered due to their size.
- Lean.instBEqImport.beq x✝¹ x✝ = false

Instances For

source
instance Lean.instHashableImport :
Hashable Import
Equations

- Lean.instHashableImport = { hash := Lean.instHashableImport.hash }

source
def Lean.instHashableImport.hash :
Import → UInt64
Equations

- Lean.instHashableImport.hash { module := a, importAll := a_1, isExported := a_2, isMeta := a_3 } = mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)

Instances For

source
instance Lean.instCoeNameImport :
Coe Name Import
Equations

- Lean.instCoeNameImport = { coe := fun (x : Lean.Name) => { module := x } }

source
instance Lean.instToStringImport :
ToString Import
Equations

- One or more equations did not get rendered due to their size.

source
structure Lean.ModuleHeader :
Type

Abstract structure of a module's header.

- imports : Array Import

  The module's direct imports (i.e., those listed in the header).

- isModule : Bool

  Whether the module is participating in the module system.

Instances For

source
instance Lean.instReprModuleHeader :
Repr ModuleHeader
Equations

- Lean.instReprModuleHeader = { reprPrec := Lean.instReprModuleHeader.repr }

source
def Lean.instReprModuleHeader.repr :
ModuleHeader → Nat → Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instInhabitedModuleHeader :
Inhabited ModuleHeader
Equations

- Lean.instInhabitedModuleHeader = { default := Lean.instInhabitedModuleHeader.default }

source
def Lean.instInhabitedModuleHeader.default :
ModuleHeader
Equations

- Lean.instInhabitedModuleHeader.default = { imports := default, isModule := default }

Instances For

source
def Lean.instToJsonModuleHeader.toJson :
ModuleHeader → Json
Equations

- Lean.instToJsonModuleHeader.toJson x✝ = Lean.Json.mkObj [[("imports", Lean.toJson x✝.imports)], [("isModule", Lean.toJson x✝.isModule)]].flatten

Instances For

source
instance Lean.instToJsonModuleHeader :
ToJson ModuleHeader
Equations

- Lean.instToJsonModuleHeader = { toJson := Lean.instToJsonModuleHeader.toJson }

source
def Lean.instFromJsonModuleHeader.fromJson :
Json → Except String ModuleHeader
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instFromJsonModuleHeader :
FromJson ModuleHeader
Equations

- Lean.instFromJsonModuleHeader = { fromJson? := Lean.instFromJsonModuleHeader.fromJson }

source
structure Lean.ImportArtifacts :
Type

Module data files used for an `import` statement. This structure is designed for efficient JSON serialization.

- ofArray :: (

- toArray : Array System.FilePath

- )

Instances For

source
instance Lean.instReprImportArtifacts :
Repr ImportArtifacts
Equations

- Lean.instReprImportArtifacts = { reprPrec := Lean.instReprImportArtifacts.repr }

source
def Lean.instReprImportArtifacts.repr :
ImportArtifacts → Nat → Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instInhabitedImportArtifacts :
Inhabited ImportArtifacts
Equations

- Lean.instInhabitedImportArtifacts = { default := Lean.instInhabitedImportArtifacts.default }

source
def Lean.instInhabitedImportArtifacts.default :
ImportArtifacts
Equations

- Lean.instInhabitedImportArtifacts.default = { toArray := default }

Instances For

source
instance Lean.instToJsonImportArtifacts :
ToJson ImportArtifacts
Equations

- Lean.instToJsonImportArtifacts = { toJson := fun (x : Lean.ImportArtifacts) => Lean.toJson x.toArray }

source
instance Lean.instFromJsonImportArtifacts :
FromJson ImportArtifacts
Equations

- Lean.instFromJsonImportArtifacts = { fromJson? := fun (x : Lean.Json) => Lean.ImportArtifacts.ofArray <$> Lean.fromJson? x }

source
def Lean.ImportArtifacts.size (arts : ImportArtifacts) :
Nat
Equations

- arts.size = arts.toArray.size

Instances For

source
def Lean.ImportArtifacts.olean? (arts : ImportArtifacts) :
Option System.FilePath
Equations

- arts.olean? = arts.toArray[0]?

Instances For

source
def Lean.ImportArtifacts.ir? (arts : ImportArtifacts) :
Option System.FilePath
Equations

- arts.ir? = arts.toArray[1]?

Instances For

source
def Lean.ImportArtifacts.oleanServer? (arts : ImportArtifacts) :
Option System.FilePath
Equations

- arts.oleanServer? = arts.toArray[2]?

Instances For

source
def Lean.ImportArtifacts.oleanPrivate? (arts : ImportArtifacts) :
Option System.FilePath
Equations

- arts.oleanPrivate? = arts.toArray[3]?

Instances For

source
def Lean.ImportArtifacts.oleanParts (inServer : Bool) (arts : ImportArtifacts) :
Array System.FilePath
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Lean.ModuleArtifacts :
Type

Files containing data for a single module.

- lean? : Option System.FilePath
- olean? : Option System.FilePath
- oleanServer? : Option System.FilePath
- oleanPrivate? : Option System.FilePath
- ilean? : Option System.FilePath
- ir? : Option System.FilePath
- c? : Option System.FilePath
- bc? : Option System.FilePath

Instances For

source
def Lean.instReprModuleArtifacts.repr :
ModuleArtifacts → Nat → Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instReprModuleArtifacts :
Repr ModuleArtifacts
Equations

- Lean.instReprModuleArtifacts = { reprPrec := Lean.instReprModuleArtifacts.repr }

source
def Lean.instInhabitedModuleArtifacts.default :
ModuleArtifacts
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instInhabitedModuleArtifacts :
Inhabited ModuleArtifacts
Equations

- Lean.instInhabitedModuleArtifacts = { default := Lean.instInhabitedModuleArtifacts.default }

source
instance Lean.instToJsonModuleArtifacts :
ToJson ModuleArtifacts
Equations

- Lean.instToJsonModuleArtifacts = { toJson := Lean.instToJsonModuleArtifacts.toJson }

source
def Lean.instToJsonModuleArtifacts.toJson :
ModuleArtifacts → Json
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instFromJsonModuleArtifacts :
FromJson ModuleArtifacts
Equations

- Lean.instFromJsonModuleArtifacts = { fromJson? := Lean.instFromJsonModuleArtifacts.fromJson }

source
def Lean.instFromJsonModuleArtifacts.fromJson :
Json → Except String ModuleArtifacts
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.ModuleArtifacts.oleanParts (arts : ModuleArtifacts) :
Array System.FilePath
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Lean.ModuleSetup :
Type

A module's setup information as described by a JSON file.

- name : Name

  Name of the module.

- isModule : Bool

  Whether the module, by default, participates in the module system. Even if `false`, a module can still choose to participate by using `module` in its header.

- imports? : Option (Array Import)

  The module's direct imports. If `none`, uses the imports from the module header.

- importArts : NameMap ImportArtifacts

  Pre-resolved artifacts of transitively imported modules.

- dynlibs : Array System.FilePath

  Dynamic libraries to load with the module.

- plugins : Array System.FilePath

  Plugins to initialize with the module.

- options : LeanOptions

  Additional options for the module.

Instances For

source
instance Lean.instReprModuleSetup :
Repr ModuleSetup
Equations

- Lean.instReprModuleSetup = { reprPrec := Lean.instReprModuleSetup.repr }

source
def Lean.instReprModuleSetup.repr :
ModuleSetup → Nat → Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instInhabitedModuleSetup :
Inhabited ModuleSetup
Equations

- Lean.instInhabitedModuleSetup = { default := Lean.instInhabitedModuleSetup.default }

source
def Lean.instInhabitedModuleSetup.default :
ModuleSetup
Equations

- Lean.instInhabitedModuleSetup.default = { name := default, isModule := default, imports? := default, importArts := default, dynlibs := default, plugins := default, options := default }

Instances For

source
instance Lean.instToJsonModuleSetup :
ToJson ModuleSetup
Equations

- Lean.instToJsonModuleSetup = { toJson := Lean.instToJsonModuleSetup.toJson }

source
def Lean.instToJsonModuleSetup.toJson :
ModuleSetup → Json
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.instFromJsonModuleSetup.fromJson :
Json → Except String ModuleSetup
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instFromJsonModuleSetup :
FromJson ModuleSetup
Equations

- Lean.instFromJsonModuleSetup = { fromJson? := Lean.instFromJsonModuleSetup.fromJson }

source
def Lean.ModuleSetup.load (path : System.FilePath) :
IO ModuleSetup

Load a `ModuleSetup` from a JSON file.

Equations

- One or more equations did not get rendered due to their size.

Instances For