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.SetOption : Type

The code represents syntax to set an option.

• stx : Lean.Syntax

  The set_option ... syntax.

instance Lean.Doc.Data.instTypeNameSetOption : TypeName SetOption

Equations

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

structure Lean.Doc.Data.Option : Type

The code represents an option.

• name : Name

  The option's name.

instance Lean.Doc.Data.instTypeNameOption : TypeName Option

Equations

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

structure Lean.Doc.Data.Atom : Type

The code represents an atom drawn from some syntax.

• name : Name

  The syntax kind's name.

• category : Name

  The syntax category

instance Lean.Doc.Data.instTypeNameAtom : TypeName Atom

Equations

• Lean.Doc.Data.instTypeNameAtom = 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✝

def Lean.Doc.name (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.tactic (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.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.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.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.kw (cat of : Ident := mkIdent Name.anonymous) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to a particular syntax kind, via one of its atoms.

It is an error if the syntax kind can't be automatically determined to contain the atom, or if multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex, detection may fail.

Specifying the category or kind using the named arguments cat and of can narrow down the process.

Use kw? to receive a suggestion of a specific kind.

Equations

• Lean.Doc.kw cat of xs = Lean.Doc.kwImpl✝ cat of false xs

def Lean.Doc.kw? (cat of : Ident := mkIdent Name.anonymous) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

A reference to a particular syntax kind, via one of its atoms.

It is an error if the syntax kind can't be automatically determined to contain the atom, or if multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex, detection may fail.

Specifying the category or kind using the named arguments cat and of can narrow down the process.

Use kw? to receive a suggestion of a specific kind.

Equations

• Lean.Doc.kw? cat of xs = Lean.Doc.kwImpl✝ cat of true xs

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.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.given (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

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

There are two syntaxes that can be used:

• {given}`x` establishes x's type as a metavariable.
• {given}`x : A uses A as the type for metavariable x.

Equations

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

def Lean.Doc.lean (name : Option Ident := none) (error warning : 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.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.leanTerm (xs : TSyntaxArray `inline) : DocM (Inline ElabInline)

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.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.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.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.suggestName (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the name role, if applicable.

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.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.suggestKw (code : StrLit) : DocM (Array CodeSuggestion)

Suggests the kw 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.