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.

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

instance Lean.Doc.instBEqSuggestionMode : BEq SuggestionMode

Equations

• Lean.Doc.instBEqSuggestionMode = { beq := Lean.Doc.instBEqSuggestionMode.beq }

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

Equations

• Lean.Doc.instBEqSuggestionMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lean.Doc.instReprSuggestionMode : Repr SuggestionMode

Equations

• Lean.Doc.instReprSuggestionMode = { reprPrec := Lean.Doc.instReprSuggestionMode.repr }

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

Equations

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

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.

Equations

• Lean.Doc.DocM = ReaderT Lean.Doc.Context (StateRefT' IO.RealWorld Lean.Doc.InternalState (StateRefT' IO.RealWorld Lean.Doc.State Lean.Elab.TermElabM))

instance Lean.Doc.instMonadStateOfInternalStateDocM : MonadStateOf InternalState DocM

Equations

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

instance Lean.Doc.instMonadStateOfStateDocM : MonadStateOf State DocM

Equations

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

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

Equations

• Lean.Doc.instMonadLiftTermElabMDocM = { monadLift := fun {α : Type} (act : Lean.Elab.TermElabM α) => Lean.Doc.instMonadLiftTermElabMDocM._private_1 act }

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

Runs a documentation elaborator in the module docstring context.

Equations

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

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.

Equations

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

@[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.

Equations

• Lean.Doc.flag default = Bool

@[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.

Equations

• Lean.Doc.many α = Array α

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

instance Lean.Doc.instToMessageDataDocArg : ToMessageData DocArg

Equations

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

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

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

Equations

• (Lean.Doc.DocArg.ident x_1).syntax = x_1.raw
• (Lean.Doc.DocArg.num n).syntax = n.raw
• (Lean.Doc.DocArg.str s).syntax = s.raw

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

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

Equations

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

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.

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

Equations

• Lean.Doc.instFromDocArgOption = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgOption._private_1 v }

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

Equations

• Lean.Doc.instFromDocArgWithSyntax = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgWithSyntax._private_1 v }

instance Lean.Doc.instFromDocArgIdent : FromDocArg Ident

Equations

• Lean.Doc.instFromDocArgIdent = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgIdent._private_1 v }

instance Lean.Doc.instFromDocArgString : FromDocArg String

Equations

• Lean.Doc.instFromDocArgString = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgString._private_1 v }

instance Lean.Doc.instFromDocArgStrLit : FromDocArg StrLit

Equations

• Lean.Doc.instFromDocArgStrLit = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgStrLit._private_1 v }

instance Lean.Doc.instFromDocArgNat : FromDocArg Nat

Equations

• Lean.Doc.instFromDocArgNat = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgNat._private_1 v }

instance Lean.Doc.instFromDocArgNumLit : FromDocArg NumLit

Equations

• Lean.Doc.instFromDocArgNumLit = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgNumLit._private_1 v }

instance Lean.Doc.instFromDocArgDataValue : FromDocArg DataValue

Equations

• Lean.Doc.instFromDocArgDataValue = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgDataValue._private_1 v }

instance Lean.Doc.instFromDocArgBool : FromDocArg Bool

Equations

• Lean.Doc.instFromDocArgBool = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgBool._private_1 v }

instance Lean.Doc.instFromDocArgMessageSeverity : FromDocArg MessageSeverity

Equations

• Lean.Doc.instFromDocArgMessageSeverity = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgMessageSeverity._private_1 v }

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

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

Equations

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

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.

Equations

• Lean.Doc.DocRoleExpander = (Lean.TSyntaxArray `inline → StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Inline Lean.ElabInline))

@[reducible, inline]

abbrev Lean.Doc.DocCommandExpander : Type

An expander for commands in docstrings.

Equations

• Lean.Doc.DocCommandExpander = StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)

@[reducible, inline]

abbrev Lean.Doc.DocDirectiveExpander : Type

An expander for directives in docstrings.

Equations

• Lean.Doc.DocDirectiveExpander = (Lean.TSyntaxArray `block → StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))

@[reducible, inline]

abbrev Lean.Doc.DocCodeBlockExpander : Type

An expander for code blocks in docstrings.

Equations

• Lean.Doc.DocCodeBlockExpander = (Lean.StrLit → StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))

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.

Equations

• Lean.Doc.CodeSuggester = (Lean.StrLit → Lean.Doc.DocM (Array Lean.Doc.CodeSuggestion))

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.

Equations

• Lean.Doc.addBuiltinCodeSuggestion decl val = ST.Ref.modify Lean.Doc.builtinCodeSuggestions fun (x : Array (Lean.Name × Lean.Doc.CodeSuggester)) => x.push (decl, val)

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

Adds a builtin documentation role.

Should be run during initialization.

Equations

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

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

Adds a builtin documentation code block.

Should be run during initialization.

Equations

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

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.

Equations

• Lean.Doc.CodeBlockSuggester = (Lean.StrLit → Lean.Doc.DocM (Array Lean.Doc.CodeBlockSuggestion))

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.

Equations

• Lean.Doc.addBuiltinCodeBlockSuggestion decl val = ST.Ref.modify Lean.Doc.builtinCodeBlockSuggestions fun (x : Array (Lean.Name × Lean.Doc.CodeBlockSuggester)) => x.push (decl, val)

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

Adds a builtin documentation directive.

Should be run during initialization.

Equations

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

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

Adds a builtin documentation command.

Should be run during initialization.

Equations

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

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.

Equations

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

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

Elaborates a sequence of blocks into a module doc snippet.

Equations

• Lean.Doc.elabModSnippet range blocks nestingLevel = do let s ← Lean.Doc.elabModSnippet'✝ range nestingLevel blocks let s ← Lean.Doc.fixupSnippet✝ s Lean.Doc.warnUnusedRefs✝ pure s