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

Equations

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

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

Equations

• Lean.Doc.instBEqPostponedImport.beq { name := a } { name := b } = (a == b)
• Lean.Doc.instBEqPostponedImport.beq x✝¹ x✝ = false

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

Equations

• Lean.Doc.instHashablePostponedImport.hash { name := a } = mixHash 0 (hash a)

instance Lean.Doc.instHashablePostponedImport : Hashable PostponedImport

Equations

• Lean.Doc.instHashablePostponedImport = { hash := Lean.Doc.instHashablePostponedImport.hash }

instance Lean.Doc.instReprPostponedImport : Repr PostponedImport

Equations

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

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

Equations

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

instance Lean.Doc.instToExprPostponedImport : ToExpr PostponedImport

Equations

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

instance Lean.Doc.instOrdPostponedImport : Ord PostponedImport

Equations

• Lean.Doc.instOrdPostponedImport = { compare := fun (x x_1 : Lean.Doc.PostponedImport) => match x, x_1 with | { name := x }, { name := y } => x.quickCmp y }

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

Equations

• Lean.Doc.instTypeNamePostponedCheck = Lean.Doc.inst✝

instance Lean.Doc.instReprPostponedCheck : Repr PostponedCheck

Equations

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

@[reducible, inline]

abbrev Lean.Doc.PostponedCheckHandler : Type

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

Equations

• Lean.Doc.PostponedCheckHandler = (Lean.Name → Dynamic → Lean.Elab.TermElabM Unit)

def Lean.Doc.checkPostponed : Elab.TermElabM Unit

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

Equations

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

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

Equations

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

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

Equations

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