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.
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.
#evalterm
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
#evale 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 mty, 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: #reducee 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 MonadLiftTmCommandElabM or MonadEvalTmCommandElabM 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
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 cannot display functions:
could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
Nat → Nat#evalfunx=>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:
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_optioneval.derive.reprfalsecould not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
Quadrant#evalQuadrant.nw
could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
Quadrant
('#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.
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 MonadEvalmCommandElabM or MonadEvalmIO instance.
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:
#check can be used to elaborate a term and check its type.
command::= ...
|#checkterm
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:
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#checkfunx=>x+x
fun x => x + x : (x : ?m.12) → ?m.19 x
syntaxTesting Type Errors
command::= ...
|#check_failureterm
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.96#check_failurefailed to synthesize
HAdd String Nat ?m.96
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command."one"+1
failed to synthesize
HAdd String Nat ?m.96
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
Nonetheless, a partially-elaborated term is available:
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.
The #print family of commands are used to query Lean for information about definitions.
syntaxPrinting Definitions
command::= ...
|#printident
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.
The resulting proof makes use of a number of axioms:
'swap_eq_swap'' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]#printaxiomsswap_eq_swap'
'swap_eq_swap'' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, 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::= ...
|#printequationsident
command::= ...
|#printeqnsident
Printing Equations
defintersperse(x:α):Listα→Listα|y::z::zs=>y::x::interspersex(z::zs)|xs=>xsequations:
@[defeq] 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#printequationsintersperse
equations:
@[defeq] 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#checkintersperse.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#checkintersperse.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.
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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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,*))?incommand
/--...-/#guard_msgsincmd captures the messages generated by the command cmd
and checks that they match the contents of the docstring.
The filters can be prefixed with the action to take:
check (the default): capture and check the message
drop: drop the message
pass: let the message pass through
If no filter is specified, checkall is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit passall at the end.
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,dropall)incmd 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
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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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 ensure that a set of test cases pass:
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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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 (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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 (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter::=A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
drop?all
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter::= ...
|A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
drop?info
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter::= ...
|A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
drop?warning
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter::= ...
|A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
drop?error
A message filter specification for #guard_msgs.
info, warning, error: capture (non-trace) messages with the given severity level.
check (the default): capture and check the message
drop: drop the message
pass: let the message pass through
If no filter is specified, checkall is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit passall at the end.
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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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, 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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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 shows 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.
When messages are large and only differ by a small amount, this can make it easier to notice where they differ.
Setting guard_msgs.diff to false 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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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 just the produced message, which can be compared with the expected message in the source file.
This can be convenient if the difference between the message is confusing or overwhelming.
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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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:
Without guard_msgs.diff, 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 `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
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:
The Repr type class is used to provide a standard representation for data that can be parsed and evaluated to obtain an equivalent value.
This is not a strict correctness criterion: for some types, especially those with embedded propositions, it is impossible to achieve.
However, the output produced by a Repr instance should be as close as possible to something that can be parsed and evaluated.
In addition to being machine-readable, this representation should be convenient for humans to understand—in particular, lines should not be too long, and nested values should be indented.
This is achieved through a two-step process:
The Repr instance produces an intermediate document of type Std.Format, which compactly represents a set of strings that differ with respect to the placement of newlines and indentation.
A rendering process selects the “best” representative from the set, according to criteria such as a desired maximum line length.
In particular, Std.Format can be built compositionally, so Repr instances don't need to take the surrounding indentation context into account.
A FormatThe API described here is an adaptation of Wadler's (Philip Wadler, 2003. “A Prettier Printer”. In The Fun of Programming, A symposium in honour of Professor Richard Bird's 60th birthday.) It has been modified to be efficient in a strict language and with support for additional features such as metadata tags. is a compact representation of a set of strings.
The most important Format operations are:
Strings
A String can be made into a Format using the text constructor.
This constructor is registered as a coercion from String to Format, so it is often unnecessary to invoke it explicitly.
textstr represents the singleton set that contains only str.
If the string contains newline characters ('\n'), then they are unconditionally inserted as newlines into the resulting output, regardless of groups.
They are, however, indented according to the current indentation level.
Appending
Two Formats can be appended using the ++ operator from the AppendFormat instance.
Groups and Newlines
The constructor line represents the set that contains both "\n"++indent and " ", where indent is a string with enough spaces to indent the line correctly.
Imperatively, it can be thought of as a newline that will be “flattened” to a space if there is sufficient room on the current line.
Newlines occur in groups: the nearest enclosing application of the group operator determines which group the newline belongs to.
By default, either all lines in a group represent "\n" or all represent " "; groups may also be configured to fill lines, in which case the minimal number of lines in the group represent "\n".
Uses of line that do not belong to a group always represent "\n".
Indentation
When a newline is inserted, the output is also indented.
nestn increases the indentation of a document by n spaces.
This is not sufficient to represent all Lean syntax, which sometimes requires that columns align exactly.
align is a document that ensures that the output string is at the current indentation level, inserting just spaces if possible, or a newline followed by spaces if needed.
Tagging
Lean's interactive features require the ability to associate output with the underlying values that they represent.
This allows Lean development environments to present elaborated terms when hovering over terms proof states or error messages, for example.
Documents can be tagged with a Nat value n using tagn; these Nats should be mapped to the underlying value in a side table.
Because all the lines belong to the same group, they will either all be rendered as spaces or all be rendered as newlines.
If only 9 characters are available, all of the lines in lst become newlines:
If only 20 characters are available, each occurrence of lst ends up on its own line.
This is because converting the outer group to newlines is sufficient to keep the string within 20 columns:
Including a newline character in a string causes the rendering process to unconditionally insert a newline.
These newlines do, however, respect the current indentation level.
The document str consists of an embedded string with two newlines:
The operators in this section are useful when there is some kind of repeated content, such as the elements of a list.
This is typically done by including line in their separator parameters, using a bracketing operator
Use pretty to construct a String.
The entire string must be constructed up front before any can be sent to a user.
Use prettyM to incrementally emit the String, using effects in some Monad.
As soon as each line is rendered, it is emitted.
This is suitable for streaming output.
The Std.ToFormat class is used to provide a standard means to format a value, with no expectation that this formatting be valid Lean syntax.
These instances are used in error messages and by some of the sequence concatenation operators.
A Repr instance describes how to represent a value as a Std.Format.
Because they should emit valid Lean syntax, these instances need to take precedence into account.
Inserting the maximal number of parentheses would work, but it makes it more difficult for humans to read the resulting output.
The first explicit parameter is the value to be represented, while the second is the precedence of the context in which it occurs.
This precedence can be used to decide whether to insert parentheses: if the precedence of the syntax being produced by the instance is greater than that of its context, parentheses are necessary.
Lean can produce an appropriate Repr instance for most types automatically using instance deriving.
In some cases, however, it's necessary to write an instance by hand:
When writing a custom Repr instance, please follow these conventions:
Precedence
Check precedence, adding parentheses as needed, and pass the correct precedence to the reprPrec instances of embedded data.
Each instance is responsible for surrounding itself in parentheses if needed; instances should generally not parenthesize recursive calls to reprPrec.
Function application has the maximum precedence, max_prec.
The helpers Repr.addAppParen and reprArg respectively insert parentheses around applications when needed and pass the appropriate precedence to function arguments.
Fully-Qualified Names
A Repr instance does have access to the set of open namespaces in a given position.
All names of constants in the environment should be fully qualified to remove ambiguity.
Default Nesting
Nested data should be indented using nestD to ensure consistent indentation across instances.
Grouping and Line Breaks
The output of every Repr instance that includes line breaks should be surrounded in a group.
Furthermore, if the resulting code contains notional expressions that are nested, a group should be inserted around each nested level.
Line breaks should usually be inserted in the following positions:
Between a constructor and each of its arguments
After :=
After ,
Between the opening and closing braces of structure instance notation and its contents
After, but not before, an infix operator
Parentheses and Brackets
Parentheses and brackets should be inserted using Std.Format.bracket or its specializations Std.Format.paren for parentheses and Std.Format.sbracket for square brackets.
These operators align the contents of the parenthesized or bracketed expression in the same way that Lean's do.
Trailing parentheses and brackets should not be placed on their own line, but rather stay with their contents.
The ReprNatOrInt instance adheres to the conventions:
The right-hand side is a function application, so it uses Repr.addAppParen to add parentheses if necessary.
Parentheses are wrapped around the entire body with no additional lines.
The entire function application is grouped, and it is nested the default amount.
The function is separated from its parameters by a use of line; this newline will usually be a space because the ReprNat and ReprInt instances are unlikely to produce long output.
Recursive calls to reprPrec pass max_prec because they are in function parameter positions, and function application has the highest precedence.
When the elements of a list are sufficiently small, it can be both difficult to read and wasteful of space to render the list with one element per line.
To improve readability, List has two Repr instances: one that uses Std.Format.bracket for its contents, and one that uses Std.Format.bracketFill.
The latter is defined after the former and is thus selected when possible; however, it requires an instance of the empty type class ReprAtom.
If the Repr instance for a type never generates spaces or newlines, then it should have a ReprAtom instance.
Lean has ReprAtom instances for types such as String, UInt8, Nat, Char, and Bool.
Auxiliary class for marking types that should be considered atomic by Repr methods.
We use it at Repr(Listα) to decide whether bracketFill should be used or not.
