Documentation

Lean.Setup

Module Setup Information #

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

structure Lean.Import :
  • 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.

Instances For
    Equations
    Equations

    Files containing data for a single module.

    Instances For
      Equations

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

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

        Load a ModuleSetup from a JSON file.

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