structure Lean.Doc.PostponedImport : Type

A name of an import that should be present for a delayed check.

• name : Name

  The module to be imported

instance Lean.Doc.instBEqPostponedImport : BEq PostponedImport

def Lean.Doc.instBEqPostponedImport.beq : PostponedImport → PostponedImport → Bool

def Lean.Doc.instHashablePostponedImport.hash : PostponedImport → UInt64

instance Lean.Doc.instHashablePostponedImport : Hashable PostponedImport

instance Lean.Doc.instReprPostponedImport : Repr PostponedImport

def Lean.Doc.instReprPostponedImport.repr : PostponedImport → Nat → Format

instance Lean.Doc.instToExprPostponedImport : ToExpr PostponedImport

instance Lean.Doc.instOrdPostponedImport : Ord PostponedImport

structure Lean.Doc.PostponedCheck : Type

A postponed check for an inline docstring element.

• handler : Name

  The handler to call to carry out the check. It should be a PostponedCheckHandler.

• imports : Array PostponedImport

  The imports that should be available when the test is carried out.

• info : Dynamic

  Information required to carry out the check.

instance Lean.Doc.instTypeNamePostponedCheck : TypeName PostponedCheck

instance Lean.Doc.instReprPostponedCheck : Repr PostponedCheck

@[reducible, inline]

abbrev Lean.Doc.PostponedCheckHandler : Type

A procedure to carry out some postponed check from a docstring.

def Lean.Doc.checkPostponed : Elab.TermElabM Unit

Runs the postponed checks in all docstrings, reporting on the result.

structure Lean.Doc.PostponedKind : Type

A postponed check that a syntax kind name exists.

• name : Name

  The kind's name.

instance Lean.Doc.instTypeNamePostponedKind : TypeName PostponedKind

structure Lean.Doc.PostponedName : Type

A name that will be checked to exist later.

• name : Name

  The name to check for.

instance Lean.Doc.instTypeNamePostponedName : TypeName PostponedName