source
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.

Equations

- Lean.Doc.kw cat of xs = do let s ← Lean.Doc.onlyCode✝ xs liftM (Lean.Doc.kwImpl✝ cat of false s)

Instances For

source
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.

Equations

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

Instances For

source
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.

Equations

- Lean.Doc.kw? cat of xs = do let s ← Lean.Doc.onlyCode✝ xs liftM (Lean.Doc.kwImpl✝ cat of true s)

Instances For

source
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.

Equations

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

Instances For

source
def Lean.Doc.checkKindExists :
PostponedCheckHandler

Checks that a syntax kind name exists.

Equations

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

Instances For

source
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.

Equations

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

Instances For

source
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.

Equations

- Lean.Doc.kw!.getArgs x✝ = do let of ← Lean.Doc.getNamed `of none let scope ← Lean.Doc.getNamed `scope Lean.Doc.DocScope.local Lean.Doc.done liftM (Lean.Doc.kw! of scope x✝)

Instances For

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

Suggests the `kw` role, if applicable.

Equations

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

Instances For