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

Equations

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

@[implicit_reducible]

instance Lean.instReprImport : Repr Import

Equations

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

@[implicit_reducible]

instance Lean.instInhabitedImport : Inhabited Import

Equations

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

@[implicit_reducible]

instance Lean.instToJsonImport : ToJson Import

Equations

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

def Lean.instToJsonImport.toJson : Import → Json

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonImport : FromJson Import

Equations

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

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

@[implicit_reducible]

instance Lean.instBEqImport : BEq Import

Equations

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

@[implicit_reducible]

instance Lean.instHashableImport : Hashable Import

Equations

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

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)

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

Equations

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

@[implicit_reducible]

instance Lean.instToStringImport : ToString Import

Equations

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

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

Equations

• Lean.instInhabitedIRPhases = { default := Lean.instInhabitedIRPhases.default }

@[implicit_reducible]

instance Lean.instBEqIRPhases : BEq IRPhases

Equations

• Lean.instBEqIRPhases = { beq := Lean.instBEqIRPhases.beq }

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

Equations

• Lean.instBEqIRPhases.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.instReprIRPhases : Repr IRPhases

Equations

• Lean.instReprIRPhases = { reprPrec := Lean.instReprIRPhases.repr }

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

Equations

• Lean.instReprIRPhases.repr Lean.IRPhases.runtime prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.IRPhases.runtime")).group prec✝
• Lean.instReprIRPhases.repr Lean.IRPhases.comptime prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.IRPhases.comptime")).group prec✝
• Lean.instReprIRPhases.repr Lean.IRPhases.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.IRPhases.all")).group prec✝

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instInhabitedModuleHeader : Inhabited ModuleHeader

Equations

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

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

@[implicit_reducible]

instance Lean.instToJsonModuleHeader : ToJson ModuleHeader

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonModuleHeader : FromJson ModuleHeader

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instReprImportArtifacts : Repr ImportArtifacts

Equations

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

@[implicit_reducible]

instance Lean.instInhabitedImportArtifacts : Inhabited ImportArtifacts

Equations

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

@[implicit_reducible]

instance Lean.instToJsonImportArtifacts : ToJson ImportArtifacts

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonImportArtifacts : FromJson ImportArtifacts

Equations

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

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

Equations

• arts.size = arts.toArray.size

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instReprModuleArtifacts : Repr ModuleArtifacts

Equations

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

@[implicit_reducible]

instance Lean.instInhabitedModuleArtifacts : Inhabited ModuleArtifacts

Equations

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

@[implicit_reducible]

instance Lean.instToJsonModuleArtifacts : ToJson ModuleArtifacts

Equations

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

def Lean.instToJsonModuleArtifacts.toJson : ModuleArtifacts → Json

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonModuleArtifacts : FromJson ModuleArtifacts

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instReprPlugin : Repr Plugin

Equations

• Lean.instReprPlugin = { reprPrec := Lean.instReprPlugin.repr }

def Lean.instToJsonPlugin.toJson : Plugin → Json

Equations

• Lean.instToJsonPlugin.toJson x✝ = Lean.Json.mkObj [[("path", Lean.toJson x✝.path)], Lean.Json.opt "initFn" x✝.initFn?].flatten

@[implicit_reducible]

instance Lean.instToJsonPlugin : ToJson Plugin

Equations

• Lean.instToJsonPlugin = { toJson := Lean.instToJsonPlugin.toJson }

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.

Equations

• Lean.Plugin.ofFilePath path = { path := path, initFn? := none }

@[implicit_reducible]

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

Equations

• Lean.Plugin.instCoeFilePath = { coe := Lean.Plugin.ofFilePath }

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Plugin.fromJson? (Lean.Json.str path) = pure (Lean.Plugin.ofFilePath { toString := path })
• Lean.Plugin.fromJson? data = throw "expected string or object"

@[implicit_reducible]

instance Lean.Plugin.instFromJson : FromJson Plugin

Equations

• Lean.Plugin.instFromJson = { fromJson? := Lean.Plugin.fromJson? }

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

Equations

• Lean.PkgId = String

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

Equations

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

@[implicit_reducible]

instance Lean.instReprModuleSetup : Repr ModuleSetup

Equations

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

@[implicit_reducible]

instance Lean.instInhabitedModuleSetup : Inhabited ModuleSetup

Equations

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

def Lean.instToJsonModuleSetup.toJson : ModuleSetup → Json

Equations

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

@[implicit_reducible]

instance Lean.instToJsonModuleSetup : ToJson ModuleSetup

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonModuleSetup : FromJson ModuleSetup

Equations

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

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.