3. Interacting with Lean🔗

Lean is designed for interactive use, rather than as a batch-mode system in which whole files are fed in and then translated to either object code or error messages. Many programming languages designed for interactive use provide a REPL,Short for “Read-Eval-Print Loop”, because code is parsed (“read”), evaluated, and the result displayed, with this process repeated as many times as desired. at which code can be input and tested, along with commands for loading source files, type checking terms, or querying the environment. Lean's interactive features are based on a different paradigm. Rather than a separate command prompt outside of the program, Lean provides commands for accomplishing the same tasks in the context of a source file. By convention, commands that are intended for interactive use rather than as part of a durable code artifact are prefixed with #.

Information from Lean commands is available in the message log, which accumulates output from the elaborator. Each entry in the message log is associated with a specific source range and has a severity. There are three severities: information is used for messages that do not indicate a problem, warning indicates a potential problem, and error indicates a definite problem. For interactive commands, results are typically returned as informational messages that are associated with the command's leading keyword.

3.1. Evaluating Terms🔗

The Lean.Parser.Command.eval : command`#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 command is used to run code as a program. In particular, it is capable of executing IO actions, it uses a call-by-value evaluation strategy, partial functions are executed, and both types and proofs are erased. Use Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions.#reduce to instead reduce terms using the reduction rules that are part of definitional equality.

syntaxEvaluating Terms

command ::= ...
    | `#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 term

command ::= ...
    | `#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! term

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

Lean.Parser.Command.eval : command`#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 always elaborates and compiles the provided term. It then checks whether the term transitively depends on any uses of sorry, in which case evaluation is terminated unless the command was invoked as Lean.Parser.Command.eval : command`#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!. This is because compiled code may rely on compile-time invariants (such as array lookups being in-bounds) that are ensured by proofs of suitable statements, and running code that contains incomplete proofs (or uses of sorry that “prove” incorrect statements) can cause Lean itself to crash.

The way the code is run depends on its type:

If the type is in the IO monad, then it is executed in a context where standard output and standard error are captured and redirected to the Lean message log. If the returned value's type is not Unit, then it is displayed as if it were the result of a non-monadic expression.
If the type is in one of the internal Lean metaprogramming monads (CommandElabM, TermElabM, MetaM, or CoreM), then it is run in the current context. For example, the environment will contain the definitions that are in scope where Lean.Parser.Command.eval : command`#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 is invoked. As with IO, the resulting value is displayed as if it were the result of a non-monadic expression. When Lean is running under Lake, its working directory (and thus the working directory for IO actions) is the current workspace.
If the type is in some other monad m, and there is a MonadLiftT m CommandElabM or MonadEvalT m CommandElabM instance, then MonadLiftT.monadLift or MonadEvalT.monadEval is used to transform the monad into one that may be run with Lean.Parser.Command.eval : command`#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, after which it is run as usual.
If the term's type is not in any of the supported monads, then it is treated as a pure value. The compiled code is run, and the result is displayed.

Auxiliary definitions or other environment modifications that result from elaborating the term in Lean.Parser.Command.eval : command`#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 are discarded. If the term is an action in a metaprogramming monad, then changes made to the environment by the running the monadic action are preserved.

Results are displayed using a ToExpr, ToString, or Repr instance, if they exist. If not, and eval.derive.repr is true, Lean attempts to derive a suitable Repr instance. It is an error if no suitable instance can be found or derived. Setting eval.pp to false disables the use of ToExpr instances by Lean.Parser.Command.eval : command`#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.

Displaying Output

could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
  Nat → Nat#eval fun x => x + 1

could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
  Nat → Nat

It is capable of deriving instances to display output that has no ToString or Repr instance:

inductive Quadrant where
  | nw | sw | se | ne

Quadrant.nw#eval Quadrant.nw

Quadrant.nw

The derived instance is not saved. Disabling eval.derive.repr causes Lean.Parser.Command.eval : command`#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 to fail:

set_option eval.derive.repr false
could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
  Quadrant#eval Quadrant.nw

could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
  Quadrant

option

eval.pp

Default value: true

('#eval' command) enables using 'ToExpr' instances to pretty print the result, otherwise uses 'Repr' or 'ToString' instances

option

eval.type

Default value: false

('#eval' command) enables pretty printing the type of the result

option

eval.derive.repr

Default value: true

('#eval' command) enables auto-deriving 'Repr' instances as a fallback

Monads can be given the ability to execute in Lean.Parser.Command.eval : command`#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 by defining a suitable MonadLiftMonadLift is described in the section on lifting monads. or MonadEval instance. Just as MonadLiftT is the transitive closure of MonadLift instances, MonadEvalT is the transitive closure of MonadEval instances. As with MonadLiftT users should not define additional instances of MonadEvalT directly.

type class

MonadEval.{u, v, w}
  (m : semiOutParam (Type u → Type v))
  (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)

Typeclass used for adapting monads. This is similar to MonadLift, but instances are allowed to make use of default state for the purpose of synthesizing such an instance, if necessary. Every MonadLift instance gives a MonadEval instance.

The purpose of this class is for the #eval command, which looks for a MonadEval m CommandElabM or MonadEval m IO instance.

Instance Constructor

MonadEval.mk.{u, v, w}

Methods

monadEval : {α : Type u} → m α → n α

Evaluates a value from monad m into monad n.

type class

MonadEvalT.{u, v, w} (m : Type u → Type v)
  (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)

The transitive closure of MonadEval.

Instance Constructor

MonadEvalT.mk.{u, v, w}

Methods

monadEval : {α : Type u} → m α → n α

Evaluates a value from monad m into monad n.

3.2. Reducing Terms🔗

The Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions.#reduce command repeatedly applies reductions to a term until no further reductions are possible. Reductions are performed under binders, but to avoid unexpected slowdowns, proofs and types are skipped unless the corresponding options to Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions.#reduce are enabled. Unlike Lean.Parser.Command.eval : command`#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 command, reduction cannot have side effects and the result is displayed as a term rather than via a ToString or Repr instance.

Generally speaking, Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions.#reduce is primarily useful for diagnosing issues with definitional equality and proof terms, while Lean.Parser.Command.eval : command`#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 is more suitable for computing the value of a term. In particular, functions defined using well-founded recursion or as partial fixpoints are either very slow to compute with the reduction engine, or will not reduce at all.

syntaxReducing Terms

command ::= ...
    | `#reduce <expression>` reduces the expression `<expression>` to its normal form. This
involves applying reduction rules until no further reduction is possible.

By default, proofs and types within the expression are not reduced. Use modifiers
`(proofs := true)`  and `(types := true)` to reduce them.
Recall that propositions are types in Lean.

**Warning:** This can be a computationally expensive operation,
especially for complex expressions.

Consider using `#eval <expression>` for simple evaluation/execution
of expressions.
#reduce ((proofs := true))? ((types := true))? term

#reduce <expression> reduces the expression <expression> to its normal form. This involves applying reduction rules until no further reduction is possible.

By default, proofs and types within the expression are not reduced. Use modifiers (proofs := true) and (types := true) to reduce them. Recall that propositions are types in Lean.

Warning: This can be a computationally expensive operation, especially for complex expressions.

Consider using #eval <expression> for simple evaluation/execution of expressions.

Reducing Functions

Reducing a term results in its normal form in Lean's logic. Because the underlying term is reduced and then displayed, there is no need for a ToString or Repr instance. Functions can be displayed just as well as any other term.

In some cases, this normal form is short and resembles a term that a person might write:

fun x => x.succ#reduce (fun x => x + 1)

fun x => x.succ

In other cases, the details of the elaboration of functions such as addition to Lean's core logic are exposed:

fun x => (Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) x).1 1#reduce (fun x => 1 + x)

fun x => (Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) x).1 1

3.3. Checking Types🔗

syntaxChecking Types

#check can be used to elaborate a term and check its type.

command ::= ...
    | #check term

If the provided term is an identifier that is the name of a global constant, then #check prints its signature. Otherwise, the term is elaborated as a Lean term and its type is printed.

Elaboration of the term in Lean.Parser.Command.check : command#check does not require that the term is fully elaborated; it may contain metavariables. If the term as written could have a type, elaboration succeeds. If a required instance could never be synthesized, then elaboration fails; synthesis problems that are due to metavariables do not block elaboration.

#check and Underdetermined Types

In this example, the type of the list's elements is not determined, so the type contains a metavariable:

fun x => [x] : ?m.9 → List ?m.9#check fun x => [x]

fun x => [x] : ?m.9 → List ?m.9

In this example, both the type of the terms being added and the result type of the addition are unknown, because HAdd allows terms of different types to be added. Behind the scenes, a metavariable represents the unknown HAdd instance.

fun x => x + x : (x : ?m.12) → ?m.19 x#check fun x => x + x

fun x => x + x : (x : ?m.12) → ?m.19 x

syntaxTesting Type Errors

command ::= ...
    | #check_failure term

This variant of Lean.Parser.Command.check : command#check elaborates the term using the same process as Lean.Parser.Command.check : command#check. If elaboration succeeds, it is an error; if it fails, there is no error. The partially-elaborated term and any type information that was discovered are added to the message log.

Checking for Type Errors

Attempting to add a string to a natural number fails, as expected:

"one" + 1 : ?m.32#check_failure failed to synthesize
  HAdd String Nat ?m.32

Additional diagnostic information may be available using the `set_option diagnostics true` command."one" + 1

failed to synthesize
  HAdd String Nat ?m.32

Additional diagnostic information may be available using the `set_option diagnostics true` command.

Nonetheless, a partially-elaborated term is available:

"one" + 1 : ?m.32

3.4. Synthesizing Instances🔗

syntaxSynthesizing Instances

command ::= ...
    | #synth term

The Lean.Parser.Command.synth : command#synth command attempts to synthesize an instance for the provided class. If it succeeds, then the resulting instance term is output.

3.5. Querying the Context🔗

The #print family of commands are used to query Lean for information about definitions.

syntaxPrinting Definitions

command ::= ...
    | #print ident

Prints the definition of a constant.

Printing a definition with Lean.Parser.Command.print : command#print prints the definition as a term. Theorems that were proved using tactics may be very large when printed as terms.

syntaxPrinting Strings

command ::= ...
    | #print str

Adds the string literal to Lean's message log.

syntaxPrinting Axioms

command ::= ...
    | #print axioms ident

Lists all axioms that the constant transitively relies on.

Printing Axioms

These two functions each swap the elements in a pair of bitvectors:

def swap (x y : BitVec 32) : BitVec 32 × BitVec 32 :=
  (y, x)

def swap' (x y : BitVec 32) : BitVec 32 × BitVec 32 :=
  let x := x ^^^ y
  let y := x ^^^ y
  let x := x ^^^ y
  (x, y)

They can be proven equal using function extensionality, the simplifier, and bv_decide:

theorem swap_eq_swap' : swap = swap' := by⊢ swap = swap'
  funext x yh.hx:BitVec 32y:BitVec 32⊢ swap x y = swap' x y
  simp only [swap, swap', Prod.mk.injEq]h.hx:BitVec 32y:BitVec 32⊢ y = x ^^^ y ^^^ (x ^^^ y ^^^ y) ∧ x = x ^^^ y ^^^ y
  bv_decideAll goals completed! 🐙

The resulting proof makes use of a number of axioms:

'swap_eq_swap'' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]#print axioms swap_eq_swap'

'swap_eq_swap'' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]

syntaxPrinting Equations

The command Lean.Parser.Command.printEqns : command#print equations, which can be abbreviated Lean.Parser.Command.printEqns : command#print eqns, displays the equational lemmas for a function.

command ::= ...
    | #print equations ident

command ::= ...
    | #print eqns ident

Printing Equations

def intersperse (x : α) : List α → List α
  | y :: z :: zs => y :: x :: intersperse x (z :: zs)
  | xs => xs

equations:
theorem intersperse.eq_1.{u_1} : ∀ {α : Type u_1} (x y z : α) (zs : List α),
  intersperse x (y :: z :: zs) = y :: x :: intersperse x (z :: zs)
theorem intersperse.eq_2.{u_1} : ∀ {α : Type u_1} (x : α) (x_1 : List α),
  (∀ (y z : α) (zs : List α), x_1 = y :: z :: zs → False) → intersperse x x_1 = x_1#print equations intersperse

equations:
theorem intersperse.eq_1.{u_1} : ∀ {α : Type u_1} (x y z : α) (zs : List α),
  intersperse x (y :: z :: zs) = y :: x :: intersperse x (z :: zs)
theorem intersperse.eq_2.{u_1} : ∀ {α : Type u_1} (x : α) (x_1 : List α),
  (∀ (y z : α) (zs : List α), x_1 = y :: z :: zs → False) → intersperse x x_1 = x_1

It does not print the defining equation, nor the unfolding equation:

intersperse.eq_def.{u_1} {α : Type u_1} (x : α) (x✝ : List α) :
  intersperse x x✝ =
    match x✝ with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs#check intersperse.eq_def

intersperse.eq_def.{u_1} {α : Type u_1} (x : α) (x✝ : List α) :
  intersperse x x✝ =
    match x✝ with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs

intersperse.eq_unfold.{u_1} :
  @intersperse = fun {α} x x_1 =>
    match x_1 with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs#check intersperse.eq_unfold

intersperse.eq_unfold.{u_1} :
  @intersperse = fun {α} x x_1 =>
    match x_1 with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs

syntaxScope Information

#where gives a description of the state of the current scope scope. This includes the current namespace, open namespaces, universe and variable commands, and options set with set_option.

command ::= ...
    | `#where` gives a description of the state of the current scope scope.
This includes the current namespace, `open` namespaces, `universe` and `variable` commands,
and options set with `set_option`.
#where

Scope Information

The Lean.Parser.Command.where : command`#where` gives a description of the state of the current scope scope. This includes the current namespace, `open` namespaces, `universe` and `variable` commands, and options set with `set_option`.#where command displays all the modifications made to the current section scope, both in the current scope and in the scopes in which it is nested.

section
open Nat

namespace A
variable (n : Nat)
namespace B

open List
set_option pp.funBinderTypes true

namespace A.B

open Nat List

variable (n : Nat)

set_option pp.funBinderTypes true#where

end A.B
end

namespace A.B

open Nat List

variable (n : Nat)

set_option pp.funBinderTypes true

syntaxChecking the Lean Version

Shows the current Lean version. Prints Lean.versionString.

command ::= ...
    | Shows the current Lean version. Prints `Lean.versionString`. #version

3.6. Testing Output with `#guard_msgs`🔗

The Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- 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: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #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 ```lean #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.#guard_msgs command can be used to ensure that the messages output by a command are as expected. Together with the interaction commands in this section, it can be used to construct a file that will only elaborate if the output is as expected; such a file can be used as a test driver in Lake.

syntaxDocumenting Expected Output

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

Basic example:
```lean
/--
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:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#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
```lean
#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.
A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      #guard_msgs ((guardMsgsSpecElt,*))? in
      command

/-- ... -/ #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
declaration uses 'sorry'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.

Testing Return Values

def reverse : List α → List α := helper []
where
  helper acc
    | [] => acc
    | x :: xs => helper (x :: acc) xs

/-- info: [] -/
#guard_msgs in
#eval reverse ([] : List Nat)

/-- info: ['c', 'b', 'a'] -/
#guard_msgs in
#eval reverse "abc".toList

The behavior of the Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- 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: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #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 ```lean #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.#guard_msgs command can be specified in three ways:

Providing a filter that selects a subset of messages to be checked
Specifying a whitespace comparison strategy
Deciding to sort messages by their content or by the order in which they were produced

These configuration options are provided in parentheses, separated by commas.

syntaxSpecifying #guard_msgs Behavior

guardMsgsSpecElt ::=
    A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
guardMsgsFilter

guardMsgsSpecElt ::= ...
    | Whitespace handling for `#guard_msgs`:
- `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.
In all cases, leading and trailing whitespace is trimmed before matching.
whitespace := guardMsgsWhitespaceArg

guardMsgsSpecElt ::= ...
    | Message ordering for `#guard_msgs`:
- `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.
ordering := guardMsgsOrderingArg

There are three kinds of options for Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- 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: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #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 ```lean #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.#guard_msgs: filters, whitespace comparison strategies, and orderings.

syntaxOutput Filters for #guard_msgs

A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
guardMsgsFilter ::=
    A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
drop? all

A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
guardMsgsFilter ::= ...
    | A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
drop? info

A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
guardMsgsFilter ::= ...
    | A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
drop? warning

A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
guardMsgsFilter ::= ...
    | A message filter specification for `#guard_msgs`.
- `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.
These filters are processed in left-to-right order.
drop? error

A message filter specification for #guard_msgs.

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. These filters are processed in left-to-right order.

syntaxWhitespace Comparison for #guard_msgs

guardMsgsWhitespaceArg ::=
    exact

guardMsgsWhitespaceArg ::= ...
    | lax

guardMsgsWhitespaceArg ::= ...
    | normalized

Leading and trailing whitespace is always ignored when comparing messages. On top of that, the following settings are available:

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.

The option guard_msgs.diff controls the content of the error message that Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- 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: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #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 ```lean #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.#guard_msgs produces when the expected message doesn't match the produced message. By default, the error message shows the produced message, which can be compared with the expected message in the source file. When messages are large and only differ by a small amount, it can be difficult to spot the difference. Setting guard_msgs.diff to true causes Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- 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: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #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 ```lean #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.#guard_msgs to instead show a line-by-line difference, with a leading + used to indicate lines from the produced message and a leading - used to indicate lines from the expected message.

option

guard_msgs.diff

Default value: false

When true, show a diff between expected and actual messages if they don't match.

Displaying Differences

The Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- 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: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #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 ```lean #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.#guard_msgs command can be used to test definition of a rose tree Tree and a function Tree.big that creates them:

inductive Tree (α : Type u) : Type u where
  | val : α → Tree α
  | branches : List (Tree α) → Tree α

def Tree.big (n : Nat) : Tree Nat :=
  if n = 0 then .val 0
  else if n = 1 then .branches [.big 0]
  else .branches [.big (n / 2), .big (n / 3)]

However, it can be difficult to spot where test failures come from when the output is large:

/--
info: Tree.branches
  [Tree.branches
     [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 2], Tree.branches [Tree.val 0]]],
   Tree.branches
     [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]
-/
❌️ Docstring on `#guard_msgs` does not match generated message:

info: Tree.branches
  [Tree.branches
     [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]]],
   Tree.branches
     [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]#guard_msgs in
Tree.branches
  [Tree.branches
     [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]]],
   Tree.branches
     [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]#eval Tree.big 20

The evaluation produces:

Tree.branches
  [Tree.branches
     [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]]],
   Tree.branches
     [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]

while the Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- 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: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #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 ```lean #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.#guard_msgs command reports this error:

❌️ Docstring on `#guard_msgs` does not match generated message:

info: Tree.branches
  [Tree.branches
     [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]]],
   Tree.branches
     [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]

Enabling guard_msgs.diff highlights the differences instead, making the error more apparent:

set_option guard_msgs.diff true in
/--
info: Tree.branches
  [Tree.branches
     [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 2], Tree.branches [Tree.val 0]]],
   Tree.branches
     [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]
-/
❌️ Docstring on `#guard_msgs` does not match generated message:

  info: Tree.branches
    [Tree.branches
       [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
-       Tree.branches [Tree.branches [Tree.val 2], Tree.branches [Tree.val 0]]],
+       Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]]],
     Tree.branches
       [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
        Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]
#guard_msgs in
Tree.branches
  [Tree.branches
     [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]]],
   Tree.branches
     [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
      Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]#eval Tree.big 20

❌️ Docstring on `#guard_msgs` does not match generated message:

  info: Tree.branches
    [Tree.branches
       [Tree.branches [Tree.branches [Tree.branches [Tree.val 0], Tree.val 0], Tree.branches [Tree.val 0]],
-       Tree.branches [Tree.branches [Tree.val 2], Tree.branches [Tree.val 0]]],
+       Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]]],
     Tree.branches
       [Tree.branches [Tree.branches [Tree.val 0], Tree.branches [Tree.val 0]],
        Tree.branches [Tree.branches [Tree.val 0], Tree.val 0]]]

3. Interacting with Lean🔗

3.1. Evaluating Terms🔗

Instance Constructor

Methods

Instance Constructor

Methods

3.2. Reducing Terms🔗

3.3. Checking Types🔗

3.4. Synthesizing Instances🔗

3.5. Querying the Context🔗

3.6. Testing Output with #guard_msgs🔗

3.6. Testing Output with `#guard_msgs`🔗