structure Lean.Doc.InternalState : Type

The internal state used by docstring elaboration

• footnotes : Std.HashMap String (Ref (Lean.Doc.Inline Lean.ElabInline))
• urls : Std.HashMap String (Ref String)
• deferred : Array Lean.Doc.DeferredCheck

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

  The local instances.

  The MonadLift TermElabM DocM instance runs the lifted action with these instances, 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.

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

Equations

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

@[instance_reducible]

instance Lean.Doc.instBEqSuggestionMode : BEq SuggestionMode

Equations

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

@[instance_reducible]

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_reducible]

instance Lean.Doc.instMonadStateOfInternalStateDocM : MonadStateOf InternalState DocM

Equations

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

@[instance_reducible]

instance Lean.Doc.instMonadStateOfStateDocM : MonadStateOf State DocM

Equations

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

@[instance_reducible]

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.addDeferredCheck (check : Dynamic) (imports : Array Name) (ref : Syntax) : DocM Nat

Records a deferred check. Deferred checks represent a docstring task that can't be carried out at the elaboration site, such as resolving a forward reference. Recorded checks include the current namespace, open namespaces, and options, but not the local context.

The origin site ref is used to record the origin of the deferred check. Returns the check's index within the current docstring, which the docstring's AST stores to refer back to it.

The saved deferred check is not associated with the docstring or module doc until it is actually added to the environment. After this call, the internal state stores Name.anonymous.

Equations

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

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

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 (α × Array DeferredCheck)

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_reducible]

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_reducible]

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_reducible]

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_reducible]

instance Lean.Doc.instFromDocArgIdent : FromDocArg Ident

Equations

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

@[instance_reducible]

instance Lean.Doc.instFromDocArgString : FromDocArg String

Equations

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

@[instance_reducible]

instance Lean.Doc.instFromDocArgStrLit : FromDocArg StrLit

Equations

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

@[instance_reducible]

instance Lean.Doc.instFromDocArgNat : FromDocArg Nat

Equations

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

@[instance_reducible]

instance Lean.Doc.instFromDocArgNumLit : FromDocArg NumLit

Equations

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

@[instance_reducible]

instance Lean.Doc.instFromDocArgDataValue : FromDocArg DataValue

Equations

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

@[instance_reducible]

instance Lean.Doc.instFromDocArgBool : FromDocArg Bool

Equations

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

@[instance_reducible]

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

def Lean.Doc.registerDocMVar (extension : Name) (e : Expr) (ref : Syntax) (location : MessageData) : Elab.TermElabM Unit

Registers a single MVarErrorInfo so that, if any metavariable in e remains unresolved at the end of document elaboration, one error is emitted at ref naming the documentation extension (the constant implementing the role/code block, e.g. Lean.Doc.given) and the supplied location (e.g. "type of variable xs") that contained the hole. The element name is rendered via docElementMessage. Roles and code blocks use this to attach a diagnostic to the syntax that introduced the variable, in addition to the standard placeholder errors that the underlying elaborator emits for unsolved metas.

Equations

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