Module Setup Information

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

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.

instance Lean.instReprImport : Repr Import

instance Lean.instInhabitedImport : Inhabited Import

instance Lean.instToJsonImport : ToJson Import

instance Lean.instFromJsonImport : FromJson Import

instance Lean.instCoeNameImport : Coe Name Import

instance Lean.instToStringImport : ToString Import

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

instance Lean.instReprModuleArtifacts : Repr ModuleArtifacts

instance Lean.instInhabitedModuleArtifacts : Inhabited ModuleArtifacts

instance Lean.instToJsonModuleArtifacts : ToJson ModuleArtifacts

instance Lean.instFromJsonModuleArtifacts : FromJson ModuleArtifacts

structure Lean.ModuleSetup : Type

A module's setup information as described by a JSON file. Supersedes the module's header when the --setup CLI option is used.

• name : Name

  Name of the module.

• isModule : Bool

  Whether the module is participating in the module system.

• imports : Array Import
• modules : NameMap ModuleArtifacts

  Pre-resolved artifacts of related modules (e.g., this module's transitive imports).

• 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.

instance Lean.instReprModuleSetup : Repr ModuleSetup

instance Lean.instInhabitedModuleSetup : Inhabited ModuleSetup

instance Lean.instToJsonModuleSetup : ToJson ModuleSetup

instance Lean.instFromJsonModuleSetup : FromJson ModuleSetup

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

Load a ModuleSetup from a JSON file.