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

Equations

• Lean.Doc.Data.instTypeNameAtom = Lean.Doc.Data.inst✝

def Lean.Doc.kw (cat of : Ident := mkIdent Name.anonymous) (xs : TSyntaxArray `Lean.Doc.Parser.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)

def Lean.Doc.kw.getArgs : TSyntaxArray `Lean.Doc.Parser.inline → StateT (Array (TSyntax `Lean.Doc.Parser.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.

def Lean.Doc.kw? (cat of : Ident := mkIdent Name.anonymous) (xs : TSyntaxArray `Lean.Doc.Parser.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)

def Lean.Doc.kw?.getArgs : TSyntaxArray `Lean.Doc.Parser.inline → StateT (Array (TSyntax `Lean.Doc.Parser.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.

def Lean.Doc.checkKindExists : DeferredCheckHandler

Checks that a syntax kind name exists.

Equations

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

def Lean.Doc.kw! (of : Option Ident := none) (scope : DocScope := DocScope.local) (xs : TSyntaxArray `Lean.Doc.Parser.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.

def Lean.Doc.kw!.getArgs : TSyntaxArray `Lean.Doc.Parser.inline → StateT (Array (TSyntax `Lean.Doc.Parser.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.takeNamed `of none let scope ← Lean.Doc.takeNamed `scope Lean.Doc.DocScope.local Lean.Doc.noMoreArgs liftM (Lean.Doc.kw! of scope x✝)

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

Suggests the kw role, if applicable.

Equations

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