Module Setup Information #
Data types used by Lean module headers and the --setup
CLI.
Equations
- Lean.instReprImport = { reprPrec := Lean.reprImport✝ }
Equations
- Lean.instToJsonImport = { toJson := Lean.toJsonImport✝ }
Equations
- Lean.instFromJsonImport = { fromJson? := Lean.fromJsonImport✝ }
Equations
- Lean.instToStringImport = { toString := fun (imp : Lean.Import) => toString imp.module }
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
Instances For
Equations
- Lean.instReprModuleArtifacts = { reprPrec := Lean.reprModuleArtifacts✝ }
Equations
Equations
- Lean.instFromJsonModuleArtifacts = { fromJson? := Lean.fromJsonModuleArtifacts✝ }
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.
- 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.
Instances For
Equations
- Lean.instReprModuleSetup = { reprPrec := Lean.reprModuleSetup✝ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.instToJsonModuleSetup = { toJson := Lean.toJsonModuleSetup✝ }
Equations
- Lean.instFromJsonModuleSetup = { fromJson? := Lean.fromJsonModuleSetup✝ }
Load a ModuleSetup
from a JSON file.
Equations
- One or more equations did not get rendered due to their size.