structure Lean.Doc.InternalState : Type

The internal state used by docstring elaboration

• footnotes : Std.HashMap String (Lean.Doc.Ref✝ (Lean.Doc.Inline Lean.ElabInline))
• urls : Std.HashMap String (Lean.Doc.Ref✝ String)

structure Lean.Doc.State : Type

The state used by DocM.

• scopes : List Elab.Command.Scope

  The command elaboration scope stack.

  These scopes are used when running commands inside of documentation. To keep examples self-contained, these scopes are initialized for each doc comment as if it were the beginning of a Lean file.

• openDecls : List OpenDecl

  The set of open declarations presently in force.

  The MonadLift TermElabM DocM instance runs the lifted action in a context where these open declarations are used, so elaboration commands that mutate this state cause it to take effect in subsequent commands.

• lctx : LocalContext

  The local context.

  The MonadLift TermElabM DocM instance runs the lifted action in this context, so elaboration commands that mutate this state cause it to take effect in subsequent commands.

• localInstances : LocalInstances
• options : Options

  The options.

  The MonadLift TermElabM DocM instance runs the lifted action with these options, so elaboration commands that mutate this state cause it to take effect in subsequent commands.

inductive Lean.Doc.SuggestionMode : Type

Determines whether docstring suggestions are to be provided as part of editing the string or in a later report.

• interactive : SuggestionMode

  The user is currently editing the doc comment and can react to suggestions as code actions.

• batch : SuggestionMode

  The user is not editing the doc comment, and should receive suggestions as summaries.

@[implicit_reducible]

instance Lean.Doc.instBEqSuggestionMode : BEq SuggestionMode

def Lean.Doc.instBEqSuggestionMode.beq : SuggestionMode → SuggestionMode → Bool

def Lean.Doc.instReprSuggestionMode.repr : SuggestionMode → Nat → Format

@[implicit_reducible]

instance Lean.Doc.instReprSuggestionMode : Repr SuggestionMode

structure Lean.Doc.Context : Type

Context used as a reader in DocM.

• suggestionMode : SuggestionMode

  Whether suggestions should be provided interactively.

@[reducible, inline]

abbrev Lean.Doc.DocM (α : Type) : Type

The monad in which documentation is elaborated.

@[implicit_reducible]

instance Lean.Doc.instMonadStateOfInternalStateDocM : MonadStateOf InternalState DocM

@[implicit_reducible]

instance Lean.Doc.instMonadStateOfStateDocM : MonadStateOf State DocM

@[implicit_reducible]

instance Lean.Doc.instMonadLiftTermElabMDocM : MonadLift Elab.TermElabM DocM

def Lean.Doc.DocM.execForModule {α : Type} (act : DocM α) (suggestionMode : SuggestionMode := SuggestionMode.interactive) : Elab.TermElabM α

Runs a documentation elaborator in the module docstring context.

def Lean.Doc.DocM.exec {α : Type} (declName : Name) (binders : Syntax) (act : DocM α) (suggestionMode : SuggestionMode := SuggestionMode.interactive) : Elab.TermElabM α

Runs a documentation elaborator in a declaration's context, discarding changes made to the environment.

@[reducible, inline]

abbrev Lean.Doc.flag (default : Bool) : Type

Gadget that indicates that a function's parameter should be treated as a Boolean flag when used in a docstring extension.

@[reducible, inline]

abbrev Lean.Doc.many (α : Type u) : Type u

Gadget that indicates that a function's parameter should be treated as a repeated (and thus optional) named argument when used in a docstring extension.

inductive Lean.Doc.DocArg : Type

An argument provided to a docstring extension

• ident (val : Ident) : DocArg

  An identifier

• num (val : NumLit) : DocArg

  A number

• str (val : StrLit) : DocArg

  A string

@[implicit_reducible]

instance Lean.Doc.instToMessageDataDocArg : ToMessageData DocArg

def Lean.Doc.DocArg.syntax : DocArg → Syntax

Returns the syntax from which a documentation argument was drawn, typically used to report errors.

def Lean.Doc.DocArg.ofSyntax : TSyntax `arg_val → Elab.TermElabM DocArg

Converts the syntax of a documentation argument into a suitable value.

structure Lean.Doc.WithSyntax (α : Type u) : Type u

A value paired with the syntax it is derived from.

This can be used to provide hints and code actions.

• val : α

  The parsed value.

• stx : Syntax

  The syntax that the value was derived from.

class Lean.Doc.FromDocArg (α : Type) : Type

A canonical way to convert a documentation extension's argument into a Lean value of type α.

• fromDocArg : DocArg → Elab.TermElabM α

  Converts a documentation extension's argument into a Lean value.

@[implicit_reducible]

instance Lean.Doc.instFromDocArgOption {α : Type} [FromDocArg α] : FromDocArg (Option α)

@[implicit_reducible]

instance Lean.Doc.instFromDocArgWithSyntax {α : Type} [FromDocArg α] : FromDocArg (WithSyntax α)

@[implicit_reducible]

instance Lean.Doc.instFromDocArgIdent : FromDocArg Ident

@[implicit_reducible]

instance Lean.Doc.instFromDocArgString : FromDocArg String

@[implicit_reducible]

instance Lean.Doc.instFromDocArgStrLit : FromDocArg StrLit

@[implicit_reducible]

instance Lean.Doc.instFromDocArgNat : FromDocArg Nat

@[implicit_reducible]

instance Lean.Doc.instFromDocArgNumLit : FromDocArg NumLit

@[implicit_reducible]

instance Lean.Doc.instFromDocArgDataValue : FromDocArg DataValue

@[implicit_reducible]

instance Lean.Doc.instFromDocArgBool : FromDocArg Bool

@[implicit_reducible]

instance Lean.Doc.instFromDocArgMessageSeverity : FromDocArg MessageSeverity

def Lean.Doc.getPositional {α : Type} [FromDocArg α] (name : Name) : StateT (Array (TSyntax `doc_arg)) DocM α

Retrieves the next positional argument from the arguments to a documentation extension. Throws an error if no positional arguments remain.

def Lean.Doc.getNamed {α : Type} [FromDocArg α] (name : Name) (default : α) : StateT (Array (TSyntax `doc_arg)) DocM α

Retrieves a named argument from the arguments to a documentation extension. Returns default if no such named argument was provided.

def Lean.Doc.getMany {α : Type} [FromDocArg α] (name : Name) : StateT (Array (TSyntax `doc_arg)) DocM (Array α)

Retrieves a repeated named argument from the arguments to a documentation extension.

def Lean.Doc.getFlag (name : Name) (default : Bool) : StateT (Array (TSyntax `doc_arg)) DocM Bool

Retrieves a flag from the arguments to a documentation extension. Returns default if the flag is not explicit set.

def Lean.Doc.done : StateT (Array (TSyntax `doc_arg)) DocM Unit

Asserts that there are no further arguments to a documentation language extension.

opaque Lean.Doc.codeSuggestionExt : SimpleScopedEnvExtension Name NameSet

Environment extension for code suggestions

opaque Lean.Doc.codeBlockSuggestionExt : SimpleScopedEnvExtension Name NameSet

Environment extension for code block suggestions

opaque Lean.Doc.docRoleExt : SimpleScopedEnvExtension (Name × Name) (NameMap (Array Name))

Environment extension for docstring roles

@[reducible, inline]

abbrev Lean.Doc.DocRoleExpander : Type

An expander for roles in docstrings.

@[reducible, inline]

abbrev Lean.Doc.DocCommandExpander : Type

An expander for commands in docstrings.

@[reducible, inline]

abbrev Lean.Doc.DocDirectiveExpander : Type

An expander for directives in docstrings.

@[reducible, inline]

abbrev Lean.Doc.DocCodeBlockExpander : Type

An expander for code blocks in docstrings.

opaque Lean.Doc.builtinDocRoles : IO.Ref (NameMap (Array (Name × DocRoleExpander)))

Built-in docstring roles, for bootstrapping.

opaque Lean.Doc.docCodeBlockExt : SimpleScopedEnvExtension (Name × Name) (NameMap (Array Name))

Environment extension for docstring roles

opaque Lean.Doc.builtinDocCodeBlocks : IO.Ref (NameMap (Array (Name × DocCodeBlockExpander)))

Built-in docstring code blocks, for bootstrapping.

opaque Lean.Doc.docDirectiveExt : SimpleScopedEnvExtension (Name × Name) (NameMap (Array Name))

Environment extension for docstring directives

opaque Lean.Doc.builtinDocDirectives : IO.Ref (NameMap (Array (Name × DocDirectiveExpander)))

Built-in docstring directives, for bootstrapping.

opaque Lean.Doc.docCommandExt : SimpleScopedEnvExtension (Name × Name) (NameMap (Array Name))

Environment extension for docstring commands

opaque Lean.Doc.builtinDocCommands : IO.Ref (NameMap (Array (Name × DocCommandExpander)))

Built-in docstring commands, for bootstrapping.

structure Lean.Doc.CodeSuggestion : Type

A suggestion about an applicable role

• role : Name

  The name of the role to suggest.

• args : Option String

  The arguments it should receive, as a string.

• moreInfo : Option String

  More information to show users

@[reducible, inline]

abbrev Lean.Doc.CodeSuggester : Type

A provider of suggestions for code elements.

opaque Lean.Doc.builtinCodeSuggestions : IO.Ref (Array (Name × CodeSuggester))

Built-in code suggestions, for bootstrapping

def Lean.Doc.addBuiltinCodeSuggestion (decl : Name) (val : CodeSuggester) : IO Unit

Adds a builtin documentation code suggestion provider.

Should be run during initialization.

def Lean.Doc.addBuiltinDocRole (roleName wrapperName : Name) (impl : DocRoleExpander) : IO Unit

Adds a builtin documentation role.

Should be run during initialization.

def Lean.Doc.addBuiltinDocCodeBlock (blockName wrapper : Name) (impl : DocCodeBlockExpander) : IO Unit

Adds a builtin documentation code block.

Should be run during initialization.

structure Lean.Doc.CodeBlockSuggestion : Type

A suggestion about an applicable code block

• name : Name

  The name of the code block to suggest.

• args : Option String

  The arguments it should receive, as a string.

• moreInfo : Option String

  More information to show users

@[reducible, inline]

abbrev Lean.Doc.CodeBlockSuggester : Type

A provider of suggestions for code elements.

opaque Lean.Doc.builtinCodeBlockSuggestions : IO.Ref (Array (Name × CodeBlockSuggester))

Built-in code block suggestions, for bootstrapping

def Lean.Doc.addBuiltinCodeBlockSuggestion (decl : Name) (val : CodeBlockSuggester) : IO Unit

Adds a builtin documentation code suggestion provider.

Should be run during initialization.

def Lean.Doc.addBuiltinDocDirective (directiveName wrapper : Name) (impl : DocDirectiveExpander) : IO Unit

Adds a builtin documentation directive.

Should be run during initialization.

def Lean.Doc.addBuiltinDocCommand (commandName wrapper : Name) (impl : DocCommandExpander) : IO Unit

Adds a builtin documentation command.

Should be run during initialization.

partial def Lean.Doc.elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)

Elaborates the syntax of an inline document element to an actual inline document element.

partial def Lean.Doc.elabBlock (stx : TSyntax `block) : DocM (Block ElabInline ElabBlock)

Elaborates the syntax of an block-level document element to an actual block-level document element.

def Lean.Doc.elabBlocks (blocks : TSyntaxArray `block) : DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty))

Elaborates a sequence of blocks into a document.

def Lean.Doc.elabModSnippet (range : DeclarationRange) (blocks : TSyntaxArray `block) (nestingLevel : Nat) : DocM VersoModuleDocs.Snippet

Elaborates a sequence of blocks into a module doc snippet.