The #help command

The #help command can be used to list all definitions in a variety of extensible aspects of lean.

• #help option lists options (used in set_option myOption)
• #help attr lists attributes (used in @[myAttr] def foo := ...)
• #help cats lists syntax categories (like term, tactic, stx etc)
• #help cat C lists elements of syntax category C
  • #help term, #help tactic, #help conv, #help command are shorthand for #help cat term etc.
  • #help cat+ C also shows elab and macro definitions associated to the syntaxes
• #help note "some note" lists library notes for which "some note" is a prefix of the label

Most forms take an optional identifier to narrow the search; for example #help option pp shows only pp.* options. However, #help cat makes the identifier mandatory, while #help note takes a mandatory string literal, rather than an identifier.

def Batteries.Tactic.«command#help_Option___» : Lean.ParserDescr

The command #help option shows all options that have been defined in the current environment. Each option has a format like:

option pp.all : Bool := false
  (pretty printer) display coercions, implicit parameters, proof terms, fully qualified names,
  universe, and disable beta reduction and notations during pretty printing

This says that pp.all is an option which can be set to a Bool value, and the default value is false. If an option has been modified from the default using e.g. set_option pp.all true, it will appear as a (currently: true) note next to the option.

The form #help option id will show only options that begin with id.

Equations

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

def Batteries.Tactic.«command#help_AttrAttribute___» : Lean.ParserDescr

The command #help attribute (or the short form #help attr) shows all attributes that have been defined in the current environment. Each attribute has a format like:

[inline]: mark definition to always be inlined

This says that inline is an attribute that can be placed on definitions like @[inline] def foo := 1. (Individual attributes may have restrictions on where they can be applied; see the attribute's documentation for details.) Both the attribute's descr field as well as the docstring will be displayed here.

The form #help attr id will show only attributes that begin with id.

Equations

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

partial def Batteries.Tactic.getHeadTk (e : Lean.Expr) : Option String

Gets the initial string token in a parser description. For example, for a declaration like syntax "bla" "baz" term : tactic, it returns some "bla". Returns none for syntax declarations that don't start with a string constant.

def Batteries.Tactic.«command#help_Cats___» : Lean.ParserDescr

The command #help cats shows all syntax categories that have been defined in the current environment. Each syntax has a format like:

category command [Lean.Parser.initFn✝]

The name of the syntax category in this case is command, and Lean.Parser.initFn✝ is the name of the declaration that introduced it. (It is often an anonymous declaration like this, but you can click to go to the definition.) It also shows the doc string if available.

The form #help cats id will show only syntax categories that begin with id.

Equations

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

def Batteries.Tactic.«command#help_Cat+______» : Lean.ParserDescr

The command #help cat C shows all syntaxes that have been defined in syntax category C in the current environment. Each syntax has a format like:

syntax "first"... [Parser.tactic.first]
  `first | tac | ...` runs each `tac` until one succeeds, or else fails.

The quoted string is the leading token of the syntax, if applicable. It is followed by the full name of the syntax (which you can also click to go to the definition), and the documentation.

• The form #help cat C id will show only attributes that begin with id.
• The form #help cat+ C will also show information about any macros and elabs associated to the listed syntaxes.

Equations

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

def String.makeBullet (s : String) : String

format the string to be included in a single markdown bullet

Equations

• s.makeBullet = "* " ++ "\n ".intercalate (s.splitOn "\n")

def Batteries.Tactic.«command#help_Note___» : Lean.ParserDescr

#help note "foo" searches for all library notes whose label starts with "foo", then displays those library notes sorted alphabetically by label, grouped by label. The command only displays the library notes that are declared in imported files or in the same file above the line containing the command.

Equations

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

def Batteries.Tactic.«command#help_Term+____» : Lean.ParserDescr

The command #help term shows all term syntaxes that have been defined in the current environment. See #help cat for more information.

Equations

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

def Batteries.Tactic.«command#help_Tactic+____» : Lean.ParserDescr

The command #help tactic shows all tactics that have been defined in the current environment. See #help cat for more information.

Equations

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

def Batteries.Tactic.«command#help_Conv+____» : Lean.ParserDescr

The command #help conv shows all tactics that have been defined in the current environment. See #help cat for more information.

Equations

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

def Batteries.Tactic.«command#help_Command+____» : Lean.ParserDescr

The command #help command shows all commands that have been defined in the current environment. See #help cat for more information.

Equations

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