Commands

Mathlib version: 2bb0410843932d03ff2c12cd9bf2e996f514a36b

#adaptation_note

Defined in: adaptationNoteCmd

Adaptation notes are comments that are used to indicate that a piece of code has been changed to accommodate a change in Lean core. They typically require further action/maintenance to be taken in the future.

#aesop_rules

Defined in: Aesop.Frontend.Parser.showRules

#aesop_stats

Defined in: Aesop.Frontend.Parser.showStats

#allow_unused_tactic

Defined in: Mathlib.Linter.UnusedTactic.«command#allow_unused_tactic_»

#allow_unused_tactic takes an input a space-separated list of identifiers. These identifiers are then allowed by the unused tactic linter: even if these tactics do not modify goals, there will be no warning emitted. Note: for this to work, these identifiers should be the SyntaxNodeKind of each tactic.

For instance, you can allow the done and skip tactics using

#allow_unused_tactic Lean.Parser.Tactic.done Lean.Parser.Tactic.skip

Notice that you should use the SyntaxNodeKind of the tactic.

#check

Defined in: Lean.Parser.Command.check

#check_assertions

Defined in: Mathlib.AssertNotExist.«command#check_assertions!»

#check_assertions retrieves all declarations and all imports that were declared not to exist so far (including in transitively imported files) and reports their current status: * ✓ means the declaration or import exists, * × means the declaration or import does not exist.

This means that the expectation is that all checks succeed by the time #check_assertions is used, typically once all of Mathlib has been built.

If all declarations and imports are available when #check_assertions is used, then the command logs an info. Otherwise, it emits a warning.

The variant #check_assertions! only prints declarations/imports that are not present in the environment. In particular, it is silent if everything is imported, making it useful for testing.

#check_failure

Defined in: Lean.Parser.Command.check_failure

#check_simp

Defined in: Lean.Parser.checkSimp

#check_simp t ~> r checks simp reduces t to r.

#check_simp

Defined in: Lean.Parser.checkSimpFailure

#check_simp t !~> checks simp fails on reducing t.

#check_tactic

Defined in: Lean.Parser.checkTactic

#check_tactic t ~> r by commands runs the tactic sequence commands on a goal with t and sees if the resulting expression has reduced it to r.

#check_tactic_failure

Defined in: Lean.Parser.checkTacticFailure

#check_tactic_failure t by tac runs the tactic tac on a goal with t and verifies it fails.

#conv

Defined in: Mathlib.Tactic.Conv.«command#conv_=>_»

The command #conv tac => e will run a conv tactic tac on e, and display the resulting expression (discarding the proof). For example, #conv rw [true_and_iff] => True ∧ False displays False. There are also shorthand commands for several common conv tactics:

#whnf e is short for #conv whnf => e
#simp e is short for #conv simp => e
#norm_num e is short for #conv norm_num => e
#push_neg e is short for #conv push_neg => e

#discr_tree_key

Defined in: Lean.Parser.discrTreeKeyCmd

#discr_tree_key t prints the discrimination tree keys for a term t (or, if it is a single identifier, the type of that constant). It uses the default configuration for generating keys.

For example,

#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)

#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _

#discr_tree_simp_key is similar to #discr_tree_key, but treats the underlying type as one of a simp lemma, i.e. transforms it into an equality and produces the key of the left-hand side.

#discr_tree_simp_key

Defined in: Lean.Parser.discrTreeSimpKeyCmd

#discr_tree_key t prints the discrimination tree keys for a term t (or, if it is a single identifier, the type of that constant). It uses the default configuration for generating keys.

For example,

#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)

#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _

#discr_tree_simp_key is similar to #discr_tree_key, but treats the underlying type as one of a simp lemma, i.e. transforms it into an equality and produces the key of the left-hand side.

#eval

Defined in: Lean.Parser.Command.eval

#eval e evaluates the expression e by compiling and evaluating it.

The command attempts to use ToExpr, Repr, or ToString instances to print the result.
If e is a monadic value of type m ty, then the command tries to adapt the monad m to one of the monads that #eval supports, which include IO, CoreM, MetaM, TermElabM, and CommandElabM. Users can define MonadEval instances to extend the list of supported monads.

The #eval command gracefully degrades in capability depending on what is imported. Importing the Lean.Elab.Command module provides full capabilities.

Due to unsoundness, #eval refuses to evaluate expressions that depend on sorry, even indirectly, since the presence of sorry can lead to runtime instability and crashes. This check can be overridden with the #eval! e command.

Options: * If eval.pp is true (default: true) then tries to use ToExpr instances to make use of the usual pretty printer. Otherwise, only tries using Repr and ToString instances. * If eval.type is true (default: false) then pretty prints the type of the evaluated value. * If eval.derive.repr is true (default: true) then attempts to auto-derive a Repr instance when there is no other way to print the result.

See also: #reduce e for evaluation by term reduction.

#eval!

Defined in: Lean.Parser.Command.evalBang

#eval e evaluates the expression e by compiling and evaluating it.

The command attempts to use ToExpr, Repr, or ToString instances to print the result.
If e is a monadic value of type m ty, then the command tries to adapt the monad m to one of the monads that #eval supports, which include IO, CoreM, MetaM, TermElabM, and CommandElabM. Users can define MonadEval instances to extend the list of supported monads.

The #eval command gracefully degrades in capability depending on what is imported. Importing the Lean.Elab.Command module provides full capabilities.

Due to unsoundness, #eval refuses to evaluate expressions that depend on sorry, even indirectly, since the presence of sorry can lead to runtime instability and crashes. This check can be overridden with the #eval! e command.

Options: * If eval.pp is true (default: true) then tries to use ToExpr instances to make use of the usual pretty printer. Otherwise, only tries using Repr and ToString instances. * If eval.type is true (default: false) then pretty prints the type of the evaluated value. * If eval.derive.repr is true (default: true) then attempts to auto-derive a Repr instance when there is no other way to print the result.

See also: #reduce e for evaluation by term reduction.

#exit

Defined in: Lean.Parser.Command.exit

#explode

Defined in: Mathlib.Explode.«command#explode_»

#explode expr displays a proof term in a line-by-line format somewhat akin to a Fitch-style proof or the Metamath proof style.

For example, exploding the following theorem:

#explode iff_of_true

produces:

iff_of_true : ∀ {a b : Prop}, a → b → (a ↔ b)

0│         │ a         ├ Prop
1│         │ b         ├ Prop
2│         │ ha        ├ a
3│         │ hb        ├ b
4│         │ x✝        │ ┌ a
5│4,3      │ ∀I        │ a → b
6│         │ x✝        │ ┌ b
7│6,2      │ ∀I        │ b → a
8│5,7      │ Iff.intro │ a ↔ b
9│0,1,2,3,8│ ∀I        │ ∀ {a b : Prop}, a → b → (a ↔ b)

Overview

The #explode command takes the body of the theorem and decomposes it into its parts, displaying each expression constructor one at a time. The constructor is indicated in some way in column 3, and its dependencies are recorded in column 2.

These are the main constructor types:

Lambda expressions (Expr.lam). The expression fun (h : p) => s is displayed as
```
 0│    │ h   │ ┌ p
 1│**  │ **  │ │ q
 2│1,2 │ ∀I  │ ∀ (h : p), q
```
with ** a wildcard, and there can be intervening steps between 0 and 1. Nested lambda expressions can be merged, and ∀I can depend on a whole list of arguments.

Applications (Expr.app). The expression f a b c is displayed as

0│**      │ f  │ A → B → C → D
1│**      │ a  │ A
2│**      │ b  │ B
3│**      │ c  │ C
1│0,1,2,3 │ ∀E │ D

There can be intervening steps between each of these. As a special case, if f is a constant it can be omitted and the display instead looks like

0│**    │ a │ A
1│**    │ b │ B
2│**    │ c │ C
3│1,2,3 │ f │ D

Let expressions (Expr.letE) do not display in any special way, but they do ensure that in let x := v; b that v is processed first and then b, rather than first doing zeta reduction. This keeps lambda merging and application merging from making proofs with let confusing to interpret.
Everything else (constants, fvars, etc.) display x : X as
```
0│  │ x │ X
```

In more detail

The output of #explode is a Fitch-style proof in a four-column diagram modeled after Metamath proof displays like this. The headers of the columns are "Step", "Hyp", "Ref", "Type" (or "Expression" in the case of Metamath): * Step: An increasing sequence of numbers for each row in the proof, used in the Hyp fields. * Hyp: The direct children of the current step. These are step numbers for the subexpressions for this step's expression. For theorem applications, it's the theorem arguments, and for foralls it is all the bound variables and the conclusion. * Ref: The name of the theorem being applied. This is well-defined in Metamath, but in Lean there are some special steps that may have long names because the structure of proof terms doesn't exactly match this mold. * If the theorem is foo (x y : Z) : A x -> B y -> C x y: * the Ref field will contain foo, * x and y will be suppressed, because term construction is not interesting, and * the Hyp field will reference steps proving A x and B y. This corresponds to a proof term like @foo x y pA pB where pA and pB are subproofs. * In the Hyp column, suppressed terms are omitted, including terms that ought to be suppressed but are not (in particular lambda arguments). TODO: implement a configuration option to enable representing suppressed terms using an _ rather than a step number. * If the head of the proof term is a local constant or lambda, then in this case the Ref will say ∀E for forall-elimination. This happens when you have for example h : A -> B and ha : A and prove b by h ha; we reinterpret this as if it said ∀E h ha where ∀E is (n-ary) modus ponens. * If the proof term is a lambda, we will also use ∀I for forall-introduction, referencing the body of the lambda. The indentation level will increase, and a bracket will surround the proof of the body of the lambda, starting at a proof step labeled with the name of the lambda variable and its type, and ending with the ∀I step. Metamath doesn't have steps like this, but the style is based on Fitch proofs in first-order logic. * Type: This contains the type of the proof term, the theorem being proven at the current step.

Also, it is common for a Lean theorem to begin with a sequence of lambdas introducing local constants of the theorem. In order to minimize the indentation level, the ∀I steps at the end of the proof will be introduced in a group and the indentation will stay fixed. (The indentation brackets are only needed in order to delimit the scope of assumptions, and these assumptions have global scope anyway so detailed tracking is not necessary.)

#find

Defined in: Mathlib.Tactic.Find.«command#find_»

#find_home

Defined in: «command#find_home!_»

Find locations as high as possible in the import hierarchy where the named declaration could live. Using #find_home! will forcefully remove the current file. Note that this works best if used in a file with import Mathlib.

The current file could still be the only suggestion, even using #find_home! lemma. The reason is that #find_home! scans the import graph below the current file, selects all the files containing declarations appearing in lemma, excluding the current file itself and looks for all least upper bounds of such files.

For a simple example, if lemma is in a file importing only A.lean and B.lean and uses one lemma from each, then #find_home! lemma returns the current file.

#guard

Defined in: Lean.Parser.Command.guardCmd

Command to check that an expression evaluates to true.

#guard e elaborates e ensuring its type is Bool then evaluates e and checks that the result is true. The term is elaborated without variables declared using variable, since these cannot be evaluated.

Since this makes use of coercions, so long as a proposition p is decidable, one can write #guard p rather than #guard decide p. A consequence to this is that if there is decidable equality one can write #guard a = b. Note that this is not exactly the same as checking if a and b evaluate to the same thing since it uses the DecidableEq instance to do the evaluation.

Note: this uses the untrusted evaluator, so #guard passing is not a proof that the expression equals true.

#guard_expr

Defined in: Lean.Parser.Command.guardExprCmd

Command to check equality of two expressions. * #guard_expr e = e' checks that e and e' are defeq at reducible transparency. * #guard_expr e =~ e' checks that e and e' are defeq at default transparency. * #guard_expr e =ₛ e' checks that e and e' are syntactically equal. * #guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

This is a command version of the guard_expr tactic.

#guard_msgs

Defined in: Lean.guardMsgsCmd

/-- ... -/ #guard_msgs in cmd captures the messages generated by the command cmd and checks that they match the contents of the docstring.

Basic example:

/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x

This checks that there is such an error and then consumes the message.

By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings:

/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry

or only errors

#guard_msgs(error) in
example : α := sorry

In the previous example, since warnings are not captured there is a warning on sorry. We can drop the warning completely with

#guard_msgs(error, drop warning) in
example : α := sorry

In general, #guard_msgs accepts a comma-separated list of configuration clauses in parentheses:

#guard_msgs (configElt,*) in cmd

By default, the configuration list is (all, whitespace := normalized, ordering := exact).

Message filters (processed in left-to-right order): - info, warning, error: capture messages with the given severity level. - all: capture all messages (the default). - drop info, drop warning, drop error: drop messages with the given severity level. - drop all: drop every message.

Whitespace handling (after trimming leading and trailing whitespace): - whitespace := exact requires an exact whitespace match. - whitespace := normalized converts all newline characters to a space before matching (the default). This allows breaking long lines. - whitespace := lax collapses whitespace to a single space before matching.

Message ordering: - ordering := exact uses the exact ordering of the messages (the default). - ordering := sorted sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering.

For example, #guard_msgs (error, drop all) in cmd means to check warnings and drop everything else.

The command elaborator has special support for #guard_msgs for linting. The #guard_msgs itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for all top-level commands, which would include #guard_msgs itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if #guard_msgs is not present.

#help

Defined in: Batteries.Tactic.«command#help_Term+____»

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

#help

Defined in: Batteries.Tactic.«command#help_Cat+______»

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:

## first
Defined in: `Parser.tactic.first`

  `first | tac | ...` runs each `tac` until one succeeds, or else fails.
```lean
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 `macro`s and `elab`s
  associated to the listed syntaxes.

## \#help
Defined in: `Batteries.Tactic.«command#help_Command+____»`

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

## \#help
Defined in: `Batteries.Tactic.«command#help_AttrAttribute___»`

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:
```lean
[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.

#help

Defined in: Batteries.Tactic.«command#help_Note___»

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

#help

Defined in: Batteries.Tactic.«command#help_Cats___»

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.

#help

Defined in: Batteries.Tactic.«command#help_Tactic+____»

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

#help

Defined in: Batteries.Tactic.«command#help_Conv+____»

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

#help

Defined in: Batteries.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.

#html

Defined in: ProofWidgets.HtmlCommand.htmlCmd

Display a value of type Html in the infoview.

The input can be a pure value or a computation in any Lean metaprogramming monad (e.g. CommandElabM Html).

#instances

Defined in: Batteries.Tactic.Instances.instancesCmd

#instances term prints all the instances for the given class. For example, #instances Add _ gives all Add instances, and #instances Add Nat gives the Nat instance. The term can be any type that can appear in [...] binders.

Trailing underscores can be omitted, and #instances Add and #instances Add _ are equivalent; the command adds metavariables until the argument is no longer a function.

The #instances command is closely related to #synth, but #synth does the full instance synthesis algorithm and #instances does the first step of finding potential instances.

#instances

Defined in: Batteries.Tactic.Instances.«command#instances__:_»

#instances term prints all the instances for the given class. For example, #instances Add _ gives all Add instances, and #instances Add Nat gives the Nat instance. The term can be any type that can appear in [...] binders.

Trailing underscores can be omitted, and #instances Add and #instances Add _ are equivalent; the command adds metavariables until the argument is no longer a function.

The #instances command is closely related to #synth, but #synth does the full instance synthesis algorithm and #instances does the first step of finding potential instances.

#kerodon_tags

Defined in: Mathlib.StacksTag.kerodonTags

The #kerodon_tags command retrieves all declarations that have the kerodon attribute.

For each found declaration, it prints a line

'declaration_name' corresponds to tag 'declaration_tag'.

The variant #kerodon_tags! also adds the theorem statement after each summary line.

#leansearch

Defined in: LeanSearchClient.leansearch_search_cmd

Search LeanSearch from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

#lint

Defined in: Batteries.Tactic.Lint.«command#lint+-*Only___»

The command #lint runs the linters on the current file (by default).

#lint only someLinter can be used to run only a single linter.

#list_linters

Defined in: Batteries.Tactic.Lint.«command#list_linters»

The command #list_linters prints a list of all available linters.

#long_instances

Defined in: «command#long_instances_»

Lists all instances with a long name beginning with inst, gathered according to the module they are defined in. This is useful for finding automatically named instances with absurd names.

Use as #long_names or #long_names 100 to specify the length.

#long_names

Defined in: «command#long_names_»

Lists all declarations with a long name, gathered according to the module they are defined in. Use as #long_names or #long_names 100 to specify the length.

#loogle

Defined in: LeanSearchClient.loogle_cmd

Search Loogle from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.

#loogle List ?a → ?a

example := #loogle List ?a → ?a

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry

Loogle Usage

Loogle finds definitions and lemmas in various ways:

By constant: 🔍 Real.sin finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring: 🔍 \"differ\" finds all lemmas that have \"differ\" somewhere in their lemma name.

By subexpression: 🔍 _ * ( ^ ) finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in 🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map: 🔍 (?a -> ?b) -> List ?a -> List ?b 🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion: 🔍 |- tsum _ = _ * tsum _ finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example, 🔍 |- _ < _ → tsum _ < tsum _ will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search 🔍 Real.sin, \"two\", tsum, _ * , _ ^ , |- _ < _ → _ woould find all lemmas which mention the constants Real.sin and tsum, have \"two\" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

#loogle

Defined in: LeanSearchClient.just_loogle_cmd

Search Loogle from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.

#loogle List ?a → ?a

example := #loogle List ?a → ?a

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry