opaque Lean.linter.doc.deferred : Lean.Option Bool

Enables the deferred checks recorded while elaborating Verso docstrings, such as forward references.

structure Lean.Doc.PostponedName : Type

A name that a deferred check will confirm exists.

• name : Name

  The name to check for.

@[instance_reducible]

instance Lean.Doc.instTypeNamePostponedName : TypeName PostponedName

Equations

• Lean.Doc.instTypeNamePostponedName = Lean.Doc.inst✝

structure Lean.Doc.PostponedKind : Type

A syntax kind name that a deferred check will confirm exists.

• name : Name

  The kind's name.

@[instance_reducible]

instance Lean.Doc.instTypeNamePostponedKind : TypeName PostponedKind

Equations

• Lean.Doc.instTypeNamePostponedKind = Lean.Doc.inst✝

@[reducible, inline]

abbrev Lean.Doc.DeferredCheckHandler : Type

A handler that carries out a deferred docstring check, given the check's data. Each handler is expected to be applied to a single type name, rather than be able to handle any Dynamic.

Equations

• Lean.Doc.DeferredCheckHandler = (Dynamic → Lean.CoreM Unit)

opaque Lean.Doc.DeferredCheck.handlerExt : SimplePersistentEnvExtension (Name × Name) (NameMap Name)

Maps the name of a deferred check's data (the value of Dynamic.typeName) to the declaration of its DeferredCheckHandler. The data type is the dispatch key, so at most one handler is registered per type.

opaque Lean.Doc.DeferredCheck.builtinHandlers : IO.Ref (NameMap DeferredCheckHandler)

Builtin deferred check handlers, for bootstrapping. Maps a check's data type name to its handler, which is available before the defining module is imported.

def Lean.Doc.DeferredCheck.addBuiltinHandler (key : Name) (impl : DeferredCheckHandler) : IO Unit

Adds a builtin deferred check handler.

Should be run during initialization.

Equations

• Lean.Doc.DeferredCheck.addBuiltinHandler key impl = ST.Ref.modify Lean.Doc.DeferredCheck.builtinHandlers fun (x : Lean.NameMap Lean.Doc.DeferredCheckHandler) => x.insert key impl

def Lean.Doc.DeferredCheck.run (inPackage : Name → Bool) (shouldCheck : DeferredCheck → CoreM Bool := fun (x : DeferredCheck) => pure true) : CoreM (Array (Name × DeferredCheck × MessageData))

Runs the deferred docstring checks owned by modules satisfying inPackage.

Returns the checks that failed together with the module they belong to and the error that each produced. #[] indicates success.

Only checks that satisfy shouldCheck are run.

Equations

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