structure Lean.Doc.Data.Const : Type

The code represents a global constant.

• name : Name

  The constant's name.

instance Lean.Doc.Data.instTypeNameConst : TypeName Const

Equations

• Lean.Doc.Data.instTypeNameConst = Lean.Doc.Data.inst✝

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.

instance Lean.Doc.Data.instTypeNameLocal : TypeName Local

Equations

• Lean.Doc.Data.instTypeNameLocal = Lean.Doc.Data.inst✝

structure Lean.Doc.Data.Tactic : Type

The code represents a tactic.

• name : Name

  The name of the tactic's syntax kind.

instance Lean.Doc.Data.instTypeNameTactic : TypeName Tactic

Equations

• Lean.Doc.Data.instTypeNameTactic = Lean.Doc.Data.inst✝

structure Lean.Doc.Data.ConvTactic : Type

The code represents a conv tactic.

• name : Name

  The name of the tactic's syntax kind.

instance Lean.Doc.Data.instTypeNameConvTactic : TypeName ConvTactic

Equations

• Lean.Doc.Data.instTypeNameConvTactic = Lean.Doc.Data.inst✝

structure Lean.Doc.Data.Attributes : Type

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

• stx : Lean.Syntax

  The attribute syntax.

instance Lean.Doc.Data.instTypeNameAttributes : TypeName Attributes

Equations

• Lean.Doc.Data.instTypeNameAttributes = Lean.Doc.Data.inst✝

structure Lean.Doc.Data.Attribute : Type

The code represents a single attribute.

• stx : Lean.Syntax

  The attribute syntax.

instance Lean.Doc.Data.instTypeNameAttribute : TypeName Attribute

Equations

• Lean.Doc.Data.instTypeNameAttribute = Lean.Doc.Data.inst✝

structure Lean.Doc.Data.Option : Type

The code represents an option.

• name : Name

  The option's name.

• declName : Name

  The option's declaration name.

instance Lean.Doc.Data.instTypeNameOption : TypeName Option

Equations

• Lean.Doc.Data.instTypeNameOption = Lean.Doc.Data.inst✝

structure Lean.Doc.Data.SyntaxCat : Type

The code represents a syntax category name.

• name : Name

  The syntax category.

instance Lean.Doc.Data.instTypeNameSyntaxCat : TypeName SyntaxCat

Equations

• Lean.Doc.Data.instTypeNameSyntaxCat = Lean.Doc.Data.inst✝

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.

instance Lean.Doc.Data.instTypeNameSyntax : TypeName Syntax

Equations

• Lean.Doc.Data.instTypeNameSyntax = Lean.Doc.Data.inst✝

structure Lean.Doc.Data.ModuleName : Type

The code represents a module name.

• module : Name

  The module.

instance Lean.Doc.Data.instTypeNameModuleName : TypeName ModuleName

Equations

• Lean.Doc.Data.instTypeNameModuleName = Lean.Doc.Data.inst✝

def Lean.Doc.checkNameExists : PostponedCheckHandler

Checks that a name exists when it is expected to.

Equations

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

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.

Equations

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

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

Displays a name, without attempting to elaborate implicit arguments.

Equations

• Lean.Doc.name.getArgs x✝ = do let full ← Lean.Doc.getNamed `full none let scope ← Lean.Doc.getNamed `scope Lean.Doc.DocScope.local Lean.Doc.done liftM (Lean.Doc.name full scope x✝)

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

Displays a name, without attempting to elaborate implicit arguments.

Equations

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

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

Displays a name, without attempting to elaborate implicit arguments.

Equations

• Lean.Doc.module.getArgs x✝ = do let checked ← Lean.Doc.getFlag `checked true Lean.Doc.done liftM (Lean.Doc.module checked x✝)

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

Equations

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

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

Equations

• Lean.Doc.tactic.getArgs x✝ = do let checked ← Lean.Doc.getFlag `checked true Lean.Doc.done liftM (Lean.Doc.tactic checked 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)

Equations

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

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)

Equations

• Lean.Doc.conv.getArgs x✝ = do Lean.Doc.done liftM (Lean.Doc.conv x✝)

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

A reference to an attribute or attribute-application syntax.

Equations

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

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

A reference to an attribute or attribute-application syntax.

Equations

• Lean.Doc.attr.getArgs x✝ = do Lean.Doc.done liftM (Lean.Doc.attr x✝)

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

A reference to a syntax category.

Equations

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

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

A reference to a syntax category.

Equations

• Lean.Doc.syntaxCat.getArgs x✝ = do Lean.Doc.done liftM (Lean.Doc.syntaxCat x✝)

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

A description of syntax in the provided category.

Equations

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

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

A description of syntax in the provided category.

Equations

• Lean.Doc.syntax.getArgs x✝ = do let cat ← Lean.Doc.getPositional `cat Lean.Doc.done liftM (Lean.Doc.syntax cat x✝)

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.

Equations

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

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.

Equations

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

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

Elaborates a sequence of Lean commands as examples.

To make examples self-contained, elaboration ignores the surrouncing 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.

Equations

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

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

Equations

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

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.

Equations

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

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

Displays output from a named Lean code block.

Equations

• Lean.Doc.output.getArgs x✝ = do let name ← Lean.Doc.getPositional `name let severity ← Lean.Doc.getNamed `severity none Lean.Doc.done liftM (Lean.Doc.output name severity x✝)

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.

Equations

• Lean.Doc.lit xs = do let s ← Lean.Doc.onlyCode✝ xs pure (Lean.Doc.Inline.code (Lean.TSyntax.getString s))

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.

Equations

• Lean.Doc.lit.getArgs x✝ = do Lean.Doc.done liftM (Lean.Doc.lit x✝)

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.

Equations

• code.push str hl? = { code := code.code.push (str, hl?) }

instance Lean.Doc.instHAppendDocCodeString : HAppend DocCode String DocCode

Equations

• Lean.Doc.instHAppendDocCodeString = { hAppend := fun (x : Lean.Doc.DocCode) (x_1 : String) => match x, x_1 with | { code := c }, s => { code := c.push (s, none) } }

instance Lean.Doc.instAppendDocCode : Append DocCode

Equations

• Lean.Doc.instAppendDocCode = { append := fun (x x_1 : Lean.Doc.DocCode) => match x, x_1 with | { code := c1 }, { code := c2 } => { code := c1 ++ c2 } }

structure Lean.Doc.Data.LeanTerm : Type

The code represents an elaborated Lean term.

• term : DocCode

  The highlighted code to be displayed.

instance Lean.Doc.Data.instTypeNameLeanTerm : TypeName LeanTerm

Equations

• Lean.Doc.Data.instTypeNameLeanTerm = Lean.Doc.Data.inst✝

structure Lean.Doc.Data.SetOption : Type

The code represents syntax to set an option.

• term : DocCode

  The set_option ... syntax.

instance Lean.Doc.Data.instTypeNameSetOption : TypeName SetOption

Equations

• Lean.Doc.Data.instTypeNameSetOption = Lean.Doc.Data.inst✝

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.

Equations

• Lean.Doc.leanRole.getArgs x✝ = do let type ← Lean.Doc.getNamed `type none Lean.Doc.done liftM (Lean.Doc.leanRole type x✝)

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

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

Equations

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

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.

Equations

• Lean.Doc.leanTerm.getArgs x✝ = do Lean.Doc.done liftM (Lean.Doc.leanTerm x✝)

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)

Equations

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

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)

Equations

• Lean.Doc.option.getArgs x✝ = do Lean.Doc.done liftM (Lean.Doc.option x✝)

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.

Equations

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

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.

Equations

• Lean.Doc.assert'.getArgs x✝ = do Lean.Doc.done liftM (Lean.Doc.assert' x✝)

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

Asserts that an equality holds.

Equations

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

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

Asserts that an equality holds.

Equations

• Lean.Doc.assert.getArgs x✝ = do Lean.Doc.done liftM (Lean.Doc.assert x✝)

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• Lean.Doc.set_option.getArgs = do let option ← Lean.Doc.getPositional `option let value ← Lean.Doc.getPositional `value Lean.Doc.done liftM (Lean.Doc.set_option option value)

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

Constructs a link to the Lean langauge 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.

Equations

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

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

Constructs a link to the Lean langauge 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.

Equations

• Lean.Doc.manual.getArgs x✝ = do let domain ← Lean.Doc.getPositional `domain let name ← Lean.Doc.getPositional `name Lean.Doc.done liftM (Lean.Doc.manual domain name x✝)

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

Suggests the name and given roles, if applicable.

Equations

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

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

Suggests given for the syntaxes not covered by suggestName.

Equations

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

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

Suggests the lean role, if applicable.

Equations

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

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

Suggests the leanTerm code block, if applicable.

Equations

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

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

Suggests the lean code block, if applicable.

Equations

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

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

Suggests the tactic role, if applicable.

Equations

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

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

Suggests the attr role, if applicable.

Equations

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

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

Suggests the option role, if applicable.

Equations

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

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

Suggests the syntaxCat role, if applicable.

Equations

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

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

Suggests the syntax role, if applicable.

Equations

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

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

Suggests the module role, if applicable.

Equations

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