Documentation

Lean.Server.FileWorker.Utils

A document bundled with processing information. Turned into EditableDocument as soon as the reporter task has been started.

Construct a VersionedTextDocumentIdentifier from an EditableDocument -

Equations
  • ed.versionedIdentifier = { uri := ed.meta.uri, version? := some ed.meta.version }
Equations
  • One or more equations did not get rendered due to their size.
Equations