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

All forms take an optional identifier to narrow the search; for example #help option pp shows only pp.* options.

def Mathlib.Tactic.«command#help_Option___» :

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.

Instances For

source

def Mathlib.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.

Instances For

source

partial def Mathlib.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.

source

def Mathlib.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.

Instances For

source

def Mathlib.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