structure Lean.Doc.Data.Atom : Type

The code represents an atom drawn from some syntax.

• name : Name

  The syntax kind's name.

• category : Name

  The syntax category

@[instance_reducible]

instance Lean.Doc.Data.instTypeNameAtom : TypeName Atom

def Lean.Doc.kw (cat of : Ident := mkIdent Name.anonymous) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to a particular syntax kind, via one of its atoms.

It is an error if the syntax kind can't be automatically determined to contain the atom, or if multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex, detection may fail.

Specifying the category or kind using the named arguments cat and of can narrow down the process.

Use kw? to receive a suggestion of a specific kind, and kw! to disable the check.

def Lean.Doc.kw.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A reference to a particular syntax kind, via one of its atoms.

It is an error if the syntax kind can't be automatically determined to contain the atom, or if multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex, detection may fail.

Specifying the category or kind using the named arguments cat and of can narrow down the process.

Use kw? to receive a suggestion of a specific kind, and kw! to disable the check.

def Lean.Doc.kw? (cat of : Ident := mkIdent Name.anonymous) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to a particular syntax kind, via one of its atoms.

It is an error if the syntax kind can't be automatically determined to contain the atom, or if multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex, detection may fail.

Specifying the category or kind using the named arguments cat and of can narrow down the process.

Use kw? to receive a suggestion of a specific kind, and kw! to disable the check.

def Lean.Doc.kw?.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A reference to a particular syntax kind, via one of its atoms.

It is an error if the syntax kind can't be automatically determined to contain the atom, or if multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex, detection may fail.

Specifying the category or kind using the named arguments cat and of can narrow down the process.

Use kw? to receive a suggestion of a specific kind, and kw! to disable the check.

def Lean.Doc.checkKindExists : DeferredCheckHandler

Checks that a syntax kind name exists.

def Lean.Doc.kw! (of : Option Ident := none) (scope : DocScope := DocScope.local) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to a particular syntax kind, via one of its atoms.

It is an error if the syntax kind can't be automatically determined to contain the atom, or if multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex, detection may fail.

Specifying the category or kind using the named arguments cat and of can narrow down the process.

Use kw? to receive a suggestion of a specific kind, and kw! to disable the check.

def Lean.Doc.kw!.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A reference to a particular syntax kind, via one of its atoms.

It is an error if the syntax kind can't be automatically determined to contain the atom, or if multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex, detection may fail.

Specifying the category or kind using the named arguments cat and of can narrow down the process.

Use kw? to receive a suggestion of a specific kind, and kw! to disable the check.

def Lean.Doc.suggestKw (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the kw role, if applicable.