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.

@[reducible, inline]

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

The monad in which documentation is elaborated.

Equations

• Lean.Doc.DocM = 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.exec {α : Type} (declName : Name) (binders : Syntax) (act : DocM α) : Elab.TermElabM α

Runs a documentation elaborator, 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.

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

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

Adds a builtin documentation code suggestion provider.

Should be run during initialization.

Equations

• Lean.Doc.addBuiltinCodeSuggestion decl = ST.Ref.modify Lean.Doc.builtinCodeSuggestions✝ fun (x : Lean.NameSet) => x.insert decl

def Lean.Doc.addBuiltinDocRole (roleName wrapper : Name) : 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) : 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.

def Lean.Doc.addBuiltinDocDirective (directiveName wrapper : Name) : 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) : 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.