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

Instances For

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

Instances For

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

Instances For

source
instance Lean.Doc.instBEqSuggestionMode :
BEq SuggestionMode
Equations

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

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

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

Instances For

source
instance Lean.Doc.instReprSuggestionMode :
Repr SuggestionMode
Equations

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

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

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

Instances For

source
structure Lean.Doc.Context :
Type

Context used as a reader in `DocM`.

- suggestionMode : SuggestionMode

  Whether suggestions should be provided interactively.

Instances For

source
@[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))

Instances For

source
instance Lean.Doc.instMonadStateOfInternalStateDocM :
MonadStateOf InternalState DocM
Equations

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

source
instance Lean.Doc.instMonadStateOfStateDocM :
MonadStateOf State DocM
Equations

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

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

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

Instances For

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

Instances For

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

Instances For

source
@[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 α

Instances For

source
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

Instances For

source
instance Lean.Doc.instToMessageDataDocArg :
ToMessageData DocArg
Equations

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

source
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

Instances For

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

Instances For

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

Instances For

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

Instances

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

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

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

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

source
instance Lean.Doc.instFromDocArgIdent :
FromDocArg Ident
Equations

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

source
instance Lean.Doc.instFromDocArgString :
FromDocArg String
Equations

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

source
instance Lean.Doc.instFromDocArgStrLit :
FromDocArg StrLit
Equations

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

source
instance Lean.Doc.instFromDocArgNat :
FromDocArg Nat
Equations

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

source
instance Lean.Doc.instFromDocArgNumLit :
FromDocArg NumLit
Equations

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

source
instance Lean.Doc.instFromDocArgDataValue :
FromDocArg DataValue
Equations

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

source
instance Lean.Doc.instFromDocArgBool :
FromDocArg Bool
Equations

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

source
instance Lean.Doc.instFromDocArgMessageSeverity :
FromDocArg MessageSeverity
Equations

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
opaque Lean.Doc.codeSuggestionExt :
SimpleScopedEnvExtension Name NameSet

Environment extension for code suggestions

source
opaque Lean.Doc.codeBlockSuggestionExt :
SimpleScopedEnvExtension Name NameSet

Environment extension for code block suggestions

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

Environment extension for docstring roles

source
@[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))

Instances For

source
@[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)

Instances For

source
@[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))

Instances For

source
@[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))

Instances For

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

Built-in docstring roles, for bootstrapping.

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

Environment extension for docstring roles

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

Built-in docstring code blocks, for bootstrapping.

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

Environment extension for docstring directives

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

Built-in docstring directives, for bootstrapping.

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

Environment extension for docstring commands

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

Built-in docstring commands, for bootstrapping.

source
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

Instances For

source
@[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))

Instances For

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

Built-in code suggestions, for bootstrapping

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
@[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))

Instances For

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

Built-in code block suggestions, for bootstrapping

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

Instances For

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

Instances For

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

Instances For

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

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

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

Instances For

source
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

Instances For