inductive Lean.Doc.DeferredCheckSite : Type

The docstring that a deferred check was recorded in. Identifies the docstring without a source position, so that editing unrelated text doesn't change the public information of the module.

• decl (name : Name) : DeferredCheckSite

  The check was deferred in docstring of a declaration.

• moduleDoc (n : Nat) : DeferredCheckSite

  The check was deferred from the nth module docstring of the module (0-indexed).

@[instance_reducible]

instance Lean.Doc.instInhabitedDeferredCheckSite : Inhabited DeferredCheckSite

Equations

• Lean.Doc.instInhabitedDeferredCheckSite = { default := Lean.Doc.instInhabitedDeferredCheckSite.default }

@[instance_reducible]

instance Lean.Doc.instReprDeferredCheckSite : Repr DeferredCheckSite

Equations

• Lean.Doc.instReprDeferredCheckSite = { reprPrec := Lean.Doc.instReprDeferredCheckSite.repr }

def Lean.Doc.instReprDeferredCheckSite.repr : DeferredCheckSite → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Doc.instBEqDeferredCheckSite : BEq DeferredCheckSite

Equations

• Lean.Doc.instBEqDeferredCheckSite = { beq := Lean.Doc.instBEqDeferredCheckSite.beq }

def Lean.Doc.instBEqDeferredCheckSite.beq : DeferredCheckSite → DeferredCheckSite → Bool

Equations

• Lean.Doc.instBEqDeferredCheckSite.beq (Lean.Doc.DeferredCheckSite.decl a) (Lean.Doc.DeferredCheckSite.decl b) = (a == b)
• Lean.Doc.instBEqDeferredCheckSite.beq (Lean.Doc.DeferredCheckSite.moduleDoc a) (Lean.Doc.DeferredCheckSite.moduleDoc b) = (a == b)
• Lean.Doc.instBEqDeferredCheckSite.beq x✝¹ x✝ = false

structure Lean.Doc.DeferredCheck : Type

A recording of the fact that some kind of check could not be carried out when a docstring was elaborated, due to some missing information that is expected to be available in the future. This is used for forward references.

The type of the value in check selects the handler that carries out the check.

Source positions are not stored because they would shift with edits. Because deferred checks are part of the public information of a module, this would lead to needless rebuilds. The docstring is identified by site, the reference within it by index, and sourceString (the reference's source text) gives readable error messages even without an accurate location.

• site : DeferredCheckSite

  The docstring or moduledoc in which the reference appears.

• index : Nat

  The index of this reference into the deferred checks of its docstring, in source order.

• sourceString : String

  The reference's source text, to quote in error messages.

• imports : Array Name

  Modules that should be imported for the check to be meaningful (the reference's scope).

• currNamespace : Name

  The current namespace at the reference site.

• openDecls : List OpenDecl

  The open declarations in scope at the reference site.

• options : Options

  The options in effect at the reference site.

• check : Dynamic

  The check-specific data. The name of the type in the Dynamic determines which checks are to be performed.

opaque Lean.Doc.deferredCheckExt : PersistentEnvExtension DeferredCheck DeferredCheck (Array DeferredCheck)

A collection of deferred docstring checks.

While docstrings are part of the server olean for a module, deferred checks are part of the public information so they can be found by the linter.