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.

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

@[implicit_reducible]

instance Lean.instReprImport : Repr Import

@[implicit_reducible]

instance Lean.instInhabitedImport : Inhabited Import

@[implicit_reducible]

instance Lean.instToJsonImport : ToJson Import

def Lean.instToJsonImport.toJson : Import → Json

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

@[implicit_reducible]

instance Lean.instFromJsonImport : FromJson Import

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

@[implicit_reducible]

instance Lean.instBEqImport : BEq Import

@[implicit_reducible]

instance Lean.instHashableImport : Hashable Import

def Lean.instHashableImport.hash : Import → UInt64

@[extern lean_idbg_client_loop]

opaque Lean.Idbg.idbgClientLoop {α : Type} [Nonempty α] (siteId : String) (imports : Array Import) (apply : α → String) : IO Unit

@[implicit_reducible]

instance Lean.instCoeNameImport : Coe Name Import

@[implicit_reducible]

instance Lean.instToStringImport : ToString Import

inductive Lean.IRPhases : Type

Phases for which some IR is available for execution.

• runtime : IRPhases

  Available for execution in the final native code.

• comptime : IRPhases

  Available for execution during elaboration.

• all : IRPhases

  Available during run time and compile time.

@[implicit_reducible]

instance Lean.instInhabitedIRPhases : Inhabited IRPhases

@[implicit_reducible]

instance Lean.instBEqIRPhases : BEq IRPhases

def Lean.instBEqIRPhases.beq : IRPhases → IRPhases → Bool

@[implicit_reducible]

instance Lean.instReprIRPhases : Repr IRPhases

def Lean.instReprIRPhases.repr : IRPhases → Nat → Format

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.

@[implicit_reducible]

instance Lean.instReprModuleHeader : Repr ModuleHeader

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

@[implicit_reducible]

instance Lean.instInhabitedModuleHeader : Inhabited ModuleHeader

def Lean.instToJsonModuleHeader.toJson : ModuleHeader → Json

@[implicit_reducible]

instance Lean.instToJsonModuleHeader : ToJson ModuleHeader

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

@[implicit_reducible]

instance Lean.instFromJsonModuleHeader : FromJson ModuleHeader

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

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

@[implicit_reducible]

instance Lean.instReprImportArtifacts : Repr ImportArtifacts

@[implicit_reducible]

instance Lean.instInhabitedImportArtifacts : Inhabited ImportArtifacts

@[implicit_reducible]

instance Lean.instToJsonImportArtifacts : ToJson ImportArtifacts

@[implicit_reducible]

instance Lean.instFromJsonImportArtifacts : FromJson ImportArtifacts

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

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

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

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

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

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

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

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

@[implicit_reducible]

instance Lean.instReprModuleArtifacts : Repr ModuleArtifacts

@[implicit_reducible]

instance Lean.instInhabitedModuleArtifacts : Inhabited ModuleArtifacts

@[implicit_reducible]

instance Lean.instToJsonModuleArtifacts : ToJson ModuleArtifacts

def Lean.instToJsonModuleArtifacts.toJson : ModuleArtifacts → Json

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

@[implicit_reducible]

instance Lean.instFromJsonModuleArtifacts : FromJson ModuleArtifacts

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

structure Lean.Plugin : Type

A Lean plugin. Plugins are shared libraries with an initialization function.

• path : System.FilePath

  The path to the plugin's shared library.

• initFn? : Option String

  The name of the plugin initialization function symbol. If none, the symbol is derived from the file name of the shared library.

def Lean.instReprPlugin.repr : Plugin → Nat → Format

@[implicit_reducible]

instance Lean.instReprPlugin : Repr Plugin

def Lean.instToJsonPlugin.toJson : Plugin → Json

@[implicit_reducible]

instance Lean.instToJsonPlugin : ToJson Plugin

def Lean.Plugin.ofFilePath (path : System.FilePath) : Plugin

Constructs a plugin from just a shared library's path, inferring the name of the initialization function from the library's name.

@[implicit_reducible]

instance Lean.Plugin.instCoeFilePath : Coe System.FilePath Plugin

def Lean.Plugin.fromJson? (data : Json) : Except String Plugin

@[implicit_reducible]

instance Lean.Plugin.instFromJson : FromJson Plugin

@[reducible, inline]

abbrev Lean.PkgId : Type

The type of module package identifiers.

This is a String that is used to disambiguate native symbol prefixes between different packages (and different versions of the same package).

structure Lean.ModuleSetup : Type

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

• name : Name

  The name of the module.

• package? : Option PkgId

  The package to which the module belongs (if any).

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

  Plugins to initialize with the module.

• options : LeanOptions

  Additional options for the module.

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

@[implicit_reducible]

instance Lean.instReprModuleSetup : Repr ModuleSetup

@[implicit_reducible]

instance Lean.instInhabitedModuleSetup : Inhabited ModuleSetup

def Lean.instToJsonModuleSetup.toJson : ModuleSetup → Json

@[implicit_reducible]

instance Lean.instToJsonModuleSetup : ToJson ModuleSetup

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

@[implicit_reducible]

instance Lean.instFromJsonModuleSetup : FromJson ModuleSetup

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

Load a ModuleSetup from a JSON file.