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 : PostponedCheckHandler

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.