structure Lean.Doc.Data.Const : Type

The code represents a global constant.

• name : Name

  The constant's name.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameConst : TypeName Const

def Lean.Doc.Data.instReprConst.repr : Const → Nat → Format

@[implicit_reducible]

instance Lean.Doc.Data.instReprConst : Repr Const

structure Lean.Doc.Data.Local : Type

The code represents a local variable.

• name : Name

  The local variable's name.

• fvarId : FVarId

  The local variable's ID.

• lctx : LocalContext

  The local variable's context.

• type : Expr

  The local variable's type.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameLocal : TypeName Local

structure Lean.Doc.Data.Tactic : Type

The code represents a tactic.

• name : Name

  The name of the tactic's syntax kind.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameTactic : TypeName Tactic

def Lean.Doc.Data.instReprTactic.repr : Tactic → Nat → Format

@[implicit_reducible]

instance Lean.Doc.Data.instReprTactic : Repr Tactic

structure Lean.Doc.Data.ConvTactic : Type

The code represents a conv tactic.

• name : Name

  The name of the tactic's syntax kind.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameConvTactic : TypeName ConvTactic

@[implicit_reducible]

instance Lean.Doc.Data.instReprConvTactic : Repr ConvTactic

def Lean.Doc.Data.instReprConvTactic.repr : ConvTactic → Nat → Format

structure Lean.Doc.Data.Attributes : Type

The code represents an attribute application @[...].

• stx : Lean.Syntax

  The attribute syntax.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameAttributes : TypeName Attributes

def Lean.Doc.Data.instReprAttributes.repr : Attributes → Nat → Format

@[implicit_reducible]

instance Lean.Doc.Data.instReprAttributes : Repr Attributes

structure Lean.Doc.Data.Attribute : Type

The code represents a single attribute.

• stx : Lean.Syntax

  The attribute syntax.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameAttribute : TypeName Attribute

def Lean.Doc.Data.instReprAttribute.repr : Attribute → Nat → Format

@[implicit_reducible]

instance Lean.Doc.Data.instReprAttribute : Repr Attribute

structure Lean.Doc.Data.Option : Type

The code represents an option.

• name : Name

  The option's name.

• declName : Name

  The option's declaration name.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameOption : TypeName Option

def Lean.Doc.Data.instReprOption.repr : Option → Nat → Format

@[implicit_reducible]

instance Lean.Doc.Data.instReprOption : Repr Option

structure Lean.Doc.Data.SyntaxCat : Type

The code represents a syntax category name.

• name : Name

  The syntax category.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameSyntaxCat : TypeName SyntaxCat

def Lean.Doc.Data.instReprSyntaxCat.repr : SyntaxCat → Nat → Format

@[implicit_reducible]

instance Lean.Doc.Data.instReprSyntaxCat : Repr SyntaxCat

structure Lean.Doc.Data.Syntax : Type

The code represents syntax in a given category.

• category : Name

  The syntax category.

• stx : Lean.Syntax

  The parsed syntax.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameSyntax : TypeName Syntax

def Lean.Doc.Data.instReprSyntax.repr : Syntax → Nat → Format

@[implicit_reducible]

instance Lean.Doc.Data.instReprSyntax : Repr Syntax

structure Lean.Doc.Data.ModuleName : Type

The code represents a module name.

• module : Name

  The module.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameModuleName : TypeName ModuleName

@[implicit_reducible]

instance Lean.Doc.Data.instReprModuleName : Repr ModuleName

def Lean.Doc.Data.instReprModuleName.repr : ModuleName → Nat → Format

def Lean.Doc.checkNameExists : PostponedCheckHandler

Checks that a name exists when it is expected to.

def Lean.Doc.name (full : Option Ident := none) (scope : DocScope := DocScope.local) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

Displays a name, without attempting to elaborate implicit arguments.

def Lean.Doc.name.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

Displays a name, without attempting to elaborate implicit arguments.

def Lean.Doc.module (checked : flag true) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

Displays a name, without attempting to elaborate implicit arguments.

def Lean.Doc.module.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

Displays a name, without attempting to elaborate implicit arguments.

def Lean.Doc.tactic (checked : flag true) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to a tactic.

In {tactic}`T`, T can be any of the following:

• The name of a tactic syntax kind (e.g. Lean.Parser.Tactic.induction)
• The first token of a tactic (e.g. induction)
• Valid tactic syntax, potentially including antiquotations (e.g. intro $x*)

def Lean.Doc.tactic.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A reference to a tactic.

In {tactic}`T`, T can be any of the following:

• The name of a tactic syntax kind (e.g. Lean.Parser.Tactic.induction)
• The first token of a tactic (e.g. induction)
• Valid tactic syntax, potentially including antiquotations (e.g. intro $x*)

def Lean.Doc.conv (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to a conv tactic.

In {conv}`T`, T can be any of the following:

• The name of a conv tactic syntax kind (e.g. Lean.Parser.Tactic.Conv.lhs)
• Valid conv tactic syntax, potentially including antiquotations (e.g. lhs)

def Lean.Doc.conv.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A reference to a conv tactic.

In {conv}`T`, T can be any of the following:

• The name of a conv tactic syntax kind (e.g. Lean.Parser.Tactic.Conv.lhs)
• Valid conv tactic syntax, potentially including antiquotations (e.g. lhs)

def Lean.Doc.attr (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to an attribute or attribute-application syntax.

def Lean.Doc.attr.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A reference to an attribute or attribute-application syntax.

def Lean.Doc.syntaxCat (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to a syntax category.

def Lean.Doc.syntaxCat.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A reference to a syntax category.

def Lean.Doc.syntax (cat : Ident) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A description of syntax in the provided category.

def Lean.Doc.syntax.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A description of syntax in the provided category.

def Lean.Doc.given (type : Option StrLit := none) (typeIsMeta : flag false) («show» : flag true) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A metavariable to be discussed in the remainder of the docstring.

There are four syntaxes that can be used:

• {given}`x` establishes x's type as a metavariable.
• {given (type := "A")}`x` uses A as the type for metavariable x, but does not show that to readers.
• {given}`x : A` uses A as the type for metavariable x.
• {given}`x = e` establishes x as an alias for the term e

Additionally, the contents of the code literal can be repeated, with comma separators.

If the show flag is false (default true), then the metavariable is not shown in the docstring.

def Lean.Doc.given.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A metavariable to be discussed in the remainder of the docstring.

There are four syntaxes that can be used:

• {given}`x` establishes x's type as a metavariable.
• {given (type := "A")}`x` uses A as the type for metavariable x, but does not show that to readers.
• {given}`x : A` uses A as the type for metavariable x.
• {given}`x = e` establishes x as an alias for the term e

Additionally, the contents of the code literal can be repeated, with comma separators.

If the show flag is false (default true), then the metavariable is not shown in the docstring.

def Lean.Doc.givenInstance («show» : flag true) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

An instance metavariable to be discussed in the remainder of the docstring.

This is similar to {given}, but the resulting variable is marked for instance synthesis (with BinderInfo.instImplicit), and the name is optional.

There are two syntaxes that can be used:

• {givenInstance}`T` establishes an unnamed instance of type T.
• {givenInstance}`x : T` establishes a named instance x of type T.

Additionally, the contents of the code literal can be repeated, with comma separators.

If the show flag is false (default true), then the instance is not shown in the docstring.

def Lean.Doc.givenInstance.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

An instance metavariable to be discussed in the remainder of the docstring.

This is similar to {given}, but the resulting variable is marked for instance synthesis (with BinderInfo.instImplicit), and the name is optional.

There are two syntaxes that can be used:

• {givenInstance}`T` establishes an unnamed instance of type T.
• {givenInstance}`x : T` establishes a named instance x of type T.

Additionally, the contents of the code literal can be repeated, with comma separators.

If the show flag is false (default true), then the instance is not shown in the docstring.

inductive Lean.Doc.DocHighlight : Type

Semantic highlighting included on syntax from elaborated terms in documentation.

• const (name : Name) (signature : Format) : DocHighlight

  The text represents the indicated constant.

• var (userName : Name) (fvarId : FVarId) (type : Format) : DocHighlight

  The text represents the indicated local variable.

  The fvarId is not connected to a local context, but it can be useful for tracking bindings across elaborated fragments of syntax.

• field (name : Name) (signature : Format) : DocHighlight

  The text represents the name of a field. name and signature refer to the projection function.

• option (name declName : Name) : DocHighlight

  The text represents the name of a compiler option.

• keyword : DocHighlight

  The text is an atom, such as if or def.

• literal (kind : SyntaxNodeKind) (type? : Option Format) : DocHighlight

  The text is an atom that represents a literal, such as a string literal.

  isLitKind returns true for kind.

structure Lean.Doc.DocCode : Type

A code snippet contained within a docstring. Code snippets consist of a series of strings, which are optionally associated with highlighting information.

• code : Array (String × Option DocHighlight)

  The highlighted strings.

def Lean.Doc.DocCode.push (code : DocCode) (str : String) (hl? : Option DocHighlight := none) : DocCode

Adds the provided string str, with optional highlighting hl?, to the end of the code.

@[implicit_reducible]

instance Lean.Doc.instHAppendDocCodeString : HAppend DocCode String DocCode

@[implicit_reducible]

instance Lean.Doc.instAppendDocCode : Append DocCode

structure Lean.Doc.Data.LeanBlock : Type

The code represents an elaborated Lean command sequence.

• commands : DocCode

  The highlighted code to be displayed.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameLeanBlock : TypeName LeanBlock

def Lean.Doc.lean (name : Option Ident := none) (error warning : flag false) («show» : flag true) (code : StrLit) : DocM (Block ElabInline ElabBlock)

Elaborates a sequence of Lean commands as examples.

To make examples self-contained, elaboration ignores the surrounding section scopes. Modifications to the environment are preserved during a single documentation comment, and discarded afterwards.

The named argument name allows a name to be assigned to the code block; any messages created by elaboration are saved under this name.

The flags error and warning indicate that an error or warning is expected in the code.

def Lean.Doc.lean.getArgs : StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)

Elaborates a sequence of Lean commands as examples.

To make examples self-contained, elaboration ignores the surrounding section scopes. Modifications to the environment are preserved during a single documentation comment, and discarded afterwards.

The named argument name allows a name to be assigned to the code block; any messages created by elaboration are saved under this name.

The flags error and warning indicate that an error or warning is expected in the code.

def Lean.Doc.output (name : Ident) (severity : Option (WithSyntax MessageSeverity) := none) (code : StrLit) : DocM (Block ElabInline ElabBlock)

Displays output from a named Lean code block.

def Lean.Doc.output.getArgs : StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)

Displays output from a named Lean code block.

def Lean.Doc.lit (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

Indicates that a code element is intended as just a literal string, with no further meaning.

This is equivalent to a bare code element, except suggestions will not be provided for it.

def Lean.Doc.lit.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

Indicates that a code element is intended as just a literal string, with no further meaning.

This is equivalent to a bare code element, except suggestions will not be provided for it.

structure Lean.Doc.Data.LeanTerm : Type

The code represents an elaborated Lean term.

• term : DocCode

  The highlighted code to be displayed.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameLeanTerm : TypeName LeanTerm

structure Lean.Doc.Data.SetOption : Type

The code represents syntax to set an option.

• term : DocCode

  The set_option ... syntax.

@[implicit_reducible]

instance Lean.Doc.Data.instTypeNameSetOption : TypeName SetOption

def Lean.Doc.leanRole (type : Option StrLit := none) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

Treats the provided term as Lean syntax in the documentation's scope.

def Lean.Doc.leanRole.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

Treats the provided term as Lean syntax in the documentation's scope.

def Lean.Doc.leanTerm (code : StrLit) : DocM (Block ElabInline ElabBlock)

Treats the provided term as Lean syntax in the documentation's scope.

def Lean.Doc.leanTerm.getArgs : StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)

Treats the provided term as Lean syntax in the documentation's scope.

def Lean.Doc.option (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to an option.

In {option}`O`, O can be either:

• The name of an option (e.g. pp.all)
• Syntax to set an option to a particular value (e.g. set_option pp.all true)

def Lean.Doc.option.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

A reference to an option.

In {option}`O`, O can be either:

• The name of an option (e.g. pp.all)
• Syntax to set an option to a particular value (e.g. set_option pp.all true)

def Lean.Doc.assert' (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

Asserts that an equality holds.

This doesn't use the equality type because it is needed in the prelude, before the = notation is introduced.

def Lean.Doc.assert'.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

Asserts that an equality holds.

This doesn't use the equality type because it is needed in the prelude, before the = notation is introduced.

def Lean.Doc.assert (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

Asserts that an equality holds.

def Lean.Doc.assert.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

Asserts that an equality holds.

def Lean.Doc.open (n : Ident) («scoped» : flag false) (only : many Ident) : DocM (Block ElabInline ElabBlock)

Opens a namespace in the remainder of the documentation comment.

The +scoped flag causes scoped instances and attributes to be activated, but no identifiers are brought into scope. The named argument only, which can be repeated, specifies a subset of names to bring into scope from the namespace.

def Lean.Doc.open.getArgs : StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)

Opens a namespace in the remainder of the documentation comment.

The +scoped flag causes scoped instances and attributes to be activated, but no identifiers are brought into scope. The named argument only, which can be repeated, specifies a subset of names to bring into scope from the namespace.

def Lean.Doc.set_option (option : Ident) (value : DataValue) : DocM (Block ElabInline ElabBlock)

Sets the specified option to the specified value for the remainder of the comment.

def Lean.Doc.set_option.getArgs : StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)

Sets the specified option to the specified value for the remainder of the comment.

def Lean.Doc.manual (domain : Ident) (name : String) (content : TSyntaxArray `inline) : DocM (Inline ElabInline)

Constructs a link to the Lean language reference. Two positional arguments are expected:

• domain should be one of the valid domains, such as section.
• name should be the content's canonical name in the domain.

def Lean.Doc.manual.getArgs : TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)

Constructs a link to the Lean language reference. Two positional arguments are expected:

• domain should be one of the valid domains, such as section.
• name should be the content's canonical name in the domain.

def Lean.Doc.suggestName (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the name and given roles, if applicable.

def Lean.Doc.suggestGiven (code : StrLit) : DocM (Array CodeSuggestion)

Suggests given for the syntaxes not covered by suggestName.

def Lean.Doc.suggestLean (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the lean role, if applicable.

def Lean.Doc.suggestLeanTermBlock (code : StrLit) : DocM (Array CodeBlockSuggestion)

Suggests the leanTerm code block, if applicable.

def Lean.Doc.suggestLeanBlock (code : StrLit) : DocM (Array CodeBlockSuggestion)

Suggests the lean code block, if applicable.

def Lean.Doc.suggestTactic (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the tactic role, if applicable.

def Lean.Doc.suggestConvTactic (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the conv role, if applicable.

def Lean.Doc.suggestAttr (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the attr role, if applicable.

def Lean.Doc.suggestOption (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the option role, if applicable.

def Lean.Doc.suggestCat (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the syntaxCat role, if applicable.

def Lean.Doc.suggestSyntax (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the syntax role, if applicable.

def Lean.Doc.suggestModule (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the module role, if applicable.