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.
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 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
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#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
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
🔗optioneval.pp
Default value: true
('#eval' command) enables using 'ToExpr' instances to pretty print the result, otherwise uses 'Repr' or 'ToString' instances
🔗optioneval.type
Default value: false
('#eval' command) enables pretty printing the type of the result
🔗optioneval.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 classMonadEval.{u, v, w} (m : semiOutParam (Type u → Type v))
(n : Type u → Type w) : Type (max (max (u + 1) v) w) 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
Methods
monadEval : {α : Type u} → m α → n α
Evaluates a value from monad m into monad n.
🔗type classMonadEvalT.{u, v, w} (m : Type u → Type v) (n : Type u → Type w) :
Type (max (max (u + 1) v) w)
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
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 <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)
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)
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]
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
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.83#check_failure failed to synthesize
HAdd String Nat ?m.83
Additional diagnostic information may be available using the `set_option diagnostics true` command."one" + 1
Nonetheless, a partially-elaborated term is available:
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
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 identcommand ::= ...
| #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
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_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
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`.
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
syntaxChecking the Lean Version
Shows the current Lean version. Prints Lean.versionString.
command ::= ...
| Shows the current Lean version. Prints `Lean.versionString`.
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 `(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.
/-- ... -/ #guard_msgs in cmd captures the messages generated by the command cmd
and checks that they match the contents of the docstring.
Basic example:
#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:
#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 (check all, whitespace := normalized, ordering := exact).
Message filters select messages by severity:
The filters can be prefixed with the action to take:
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.
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:
def reverse : List α → List α := helper []
where
helper acc
| [] => acc
| x :: xs => helper (x :: acc) xs
#guard_msgs in
#eval reverse ([] : List Nat)
#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 `(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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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
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.
syntaxWhitespace Comparison for #guard_msgs
guardMsgsWhitespaceArg ::=
exactguardMsgsWhitespaceArg ::= ...
| laxguardMsgsWhitespaceArg ::= ...
| 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, 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 `(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 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.
🔗optionguard_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 `(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:
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:
❌️ 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:
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 `(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:
❌️ 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
❌️ 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]]]
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.
text str 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 Append Format 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.
nest n 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 tag n; these Nats should be mapped to the underlying value in a side table.
Widths and Newlines
open Std Format
The helper parenSeq creates a parenthesized sequence, with grouping and indentation to make it responsive to different output widths.
def parenSeq (xs : List Format) : Format :=
group <|
nest 2 (text "(" ++ line ++ joinSep xs line) ++
line ++
")"
This document represents a parenthesized sequence of numbers:
def lst : Format := parenSeq nums
where nums := [1, 2, 3, 4, 5].map (text s!"{·}")
Rendering it with the default line width of 120 characters places the entire sequence on one line:
( 1 2 3 4 5 )
#eval IO.println lst.pretty
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:
(
1
2
3
4
5
)
#eval IO.println (lst.pretty (width := 9))
This document contains three copies of lst in a further parenthesized sequence:
def lsts := parenSeq [lst, lst, lst]
At the default width, it remains on one line:
( ( 1 2 3 4 5 ) ( 1 2 3 4 5 ) ( 1 2 3 4 5 ) )
#eval IO.println lsts.pretty
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:
(
( 1 2 3 4 5 )
( 1 2 3 4 5 )
( 1 2 3 4 5 )
)
#eval IO.println (lsts.pretty (width := 20))
If only 10 characters are available, each number must be on its own line:
(
(
1
2
3
4
5
)
(
1
2
3
4
5
)
(
1
2
3
4
5
)
)
#eval IO.println (lsts.pretty (width := 10))
Grouping and Filling
open Std Format
The helper parenSeq creates a parenthesized sequence, with each element placed on a new line and indented:
def parenSeq (xs : List Format) : Format :=
nest 2 (text "(" ++ line ++ joinSep xs line) ++
line ++
")"
nums contains the numbers one through twenty, as a list of formats:
def nums : List Format := Nat.fold 20 (init := []) fun i _ ys => text s!"{20 - i}" :: ys
[Std.Format.text "1",
Std.Format.text "2",
Std.Format.text "3",
Std.Format.text "4",
Std.Format.text "5",
Std.Format.text "6",
Std.Format.text "7",
Std.Format.text "8",
Std.Format.text "9",
Std.Format.text "10",
Std.Format.text "11",
Std.Format.text "12",
Std.Format.text "13",
Std.Format.text "14",
Std.Format.text "15",
Std.Format.text "16",
Std.Format.text "17",
Std.Format.text "18",
Std.Format.text "19",
Std.Format.text "20"]#eval nums
Because parenSeq does not introduce any groups, the resulting document is rendered on a single line:
(
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
)
#eval IO.println (pretty (parenSeq nums))
This can be fixed by grouping them.
grouped does so with group, while filled does so with fill.
def grouped := group (parenSeq nums)
def filled := fill (parenSeq nums)
Both grouping operators cause uses of line to render as spaces.
Given sufficient space, both render on a single line:
( 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 )
#eval IO.println (pretty grouped)
( 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 )
#eval IO.println (pretty filled)
However, difference become apparent when there is not sufficient space on a single line.
Unless all newlines in a group can be spaces, none can:
(
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
)
#eval IO.println (pretty (width := 30) grouped)
Using fill, on the other hand, only inserts newlines as required to avoid being two wide:
( 1 2 3 4 5 6 7 8 9 10 11 12
13 14 15 16 17 18 19 20 )
#eval IO.println (pretty (width := 30) filled)
The behavior of fill can be seen clearly with longer sequences:
( 1 2 3 4 5 6 7 8 9 10 11 12
13 14 15 16 17 18 19 20 1 2
3 4 5 6 7 8 9 10 11 12 13 14
15 16 17 18 19 20 1 2 3 4 5
6 7 8 9 10 11 12 13 14 15 16
17 18 19 20 1 2 3 4 5 6 7 8
9 10 11 12 13 14 15 16 17 18
19 20 )
#eval IO.println (pretty (width := 30) (fill (parenSeq (nums ++ nums ++ nums ++ nums))))
Newline Characters in Strings
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:
open Std Format
def str : Format := text "abc\nxyz\n123"
Because the string does not terminate with a newline, the last line of the first string is on the same line as the first line of the second string:
abc
xyz
123abc
xyz
123
#eval IO.println (str ++ str).pretty
The empty string does not have a single unique representative in Std.Format.
All of the following represent the empty string:
-
.nil
-
.text ""
-
.text "" ++ .nil
-
.nil ++ .text ""
Use Std.Format.isEmpty to check whether a document contains zero characters, and Std.Format.isNil to specifically check whether it is the constructor Std.Format.nil.
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
These operators make it easier to achieve a consistent indentation style on top of Std.Format.nest.
These operators make it easier to achieve a consistent parenthesization style.
The ToString Std.Format instance invokes Std.Format.pretty with its default arguments.
There are two ways to render a document:
-
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.
3.7.2. Repr🔗
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.
🔗type classRepr.{u} (α : Type u) : Type u
Repr.{u} (α : Type u) : Type u
A typeclass that specifies the standard way of turning values of some type into Format.
When rendered this Format should be as close as possible to something that can be parsed as the
input value.
Instance Constructor
Methods
reprPrec : α → Nat → Std.Format
Turn a value of type α into Format at a given precedence. The precedence value can be used
to avoid parentheses if they are not necessary.
🔗def
Turn a into Format using its Repr instance. The precedence level is initially set to 0.
🔗defreprStr.{u_1} {α : Type u_1} [Repr α] (a : α) : String reprStr.{u_1} {α : Type u_1} [Repr α]
(a : α) : String
Maximal Parentheses
The type NatOrInt can contain a Nat or an Int:
inductive NatOrInt where
| nat : Nat → NatOrInt
| int : Int → NatOrInt
This Repr NatOrInt instance ensures that the output is valid Lean syntax by inserting many parentheses:
instance : Repr NatOrInt where
reprPrec x _ :=
.nestD <| .group <|
match x with
| .nat n =>
.text "(" ++ "NatOrInt.nat" ++ .line ++ "(" ++ repr n ++ "))"
| .int i =>
.text "(" ++ "NatOrInt.int" ++ .line ++ "(" ++ repr i ++ "))"
Whether it contains a Nat, a non-negative Int, or a negative Int, the result can be parsed:
open NatOrInt in
(NatOrInt.nat (3))
(NatOrInt.int (5))
(NatOrInt.int (-5))
#eval do
IO.println <| repr <| nat 3
IO.println <| repr <| int 5
IO.println <| repr <| int (-5)
However, (NatOrInt.nat (3)) is not particularly idiomatic Lean, and redundant parentheses can make it difficult to read large expressions.
The method Repr.reprPrec has the following signature:
Repr.reprPrec.{u} {α : Type u} [Repr α] : α → Nat → Std.Format
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.
3.7.2.1. How To Write a Repr Instance🔗
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.
Inductive Types with Constructors
The inductive type N.NatOrInt can contain a Nat or an Int:
namespace N
inductive NatOrInt where
| nat : Nat → NatOrInt
| int : Int → NatOrInt
The Repr NatOrInt 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 Repr Nat and Repr Int 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.
instance : Repr NatOrInt where
reprPrec
| .nat n =>
Repr.addAppParen <|
.group <| .nestD <|
"N.NatOrInt.nat" ++ .line ++ reprPrec n max_prec
| .int i =>
Repr.addAppParen <|
.group <| .nestD <|
"N.NatOrInt.int" ++ .line ++ reprPrec i max_prec
N.NatOrInt.nat 5
#eval IO.println (repr (NatOrInt.nat 5))
N.NatOrInt.int 5
#eval IO.println (repr (NatOrInt.int 5))
N.NatOrInt.int (-5)
#eval IO.println (repr (NatOrInt.int (-5)))
some (N.NatOrInt.int (-5))
#eval IO.println (repr (some (NatOrInt.int (-5))))
[N.NatOrInt.nat 0,
N.NatOrInt.nat 1,
N.NatOrInt.nat 2,
N.NatOrInt.nat 3,
N.NatOrInt.nat 4,
N.NatOrInt.nat 5,
N.NatOrInt.nat 6,
N.NatOrInt.nat 7,
N.NatOrInt.nat 8,
N.NatOrInt.nat 9]
#eval IO.println (repr <| (List.range 10).map (NatOrInt.nat))
[N.NatOrInt.nat
0,
N.NatOrInt.nat
1,
N.NatOrInt.nat
2,
N.NatOrInt.nat
3,
N.NatOrInt.nat
4,
N.NatOrInt.nat
5,
N.NatOrInt.nat
6,
N.NatOrInt.nat
7,
N.NatOrInt.nat
8,
N.NatOrInt.nat
9]
#eval IO.println (Std.Format.pretty (width := 3) (repr <| (List.range 10).map (NatOrInt.nat)))
Infix Syntax
inductive AddExpr where
| nat : Nat → AddExpr
| add : AddExpr → AddExpr → AddExpr
instance : OfNat AddExpr n where
ofNat := .nat n
instance : Add AddExpr where
add := .add
protected def AddExpr.reprPrec : AddExpr → Nat → Std.Format
| .nat n, p =>
Repr.reprPrec n p
| .add e1 e2, p =>
let out : Std.Format :=
.nestD <| .group <|
AddExpr.reprPrec e1 64 ++ " " ++ "+" ++ .line ++
AddExpr.reprPrec e2 65
if p ≥ 65 then out.paren else out
instance : Repr AddExpr := ⟨AddExpr.reprPrec⟩
2 + 3 + 4
#eval IO.println (repr (((2 + 3) + 4) : AddExpr))
2 + 3 + 4
#eval IO.println (repr ((2 + 3 + 4) : AddExpr))
2 + (3 + 4)
#eval IO.println (repr ((2 + (3 + 4)) : AddExpr))
[2 + (3 + 4), 2 + 3 + 4]
#eval IO.println (repr ([2 + (3 + 4), (2 + 3) + 4] : List AddExpr))
[2 +
(3 +
4),
2 +
3 +
4]
#eval IO.println <| (repr ([2 + (3 + 4), (2 + 3) + 4] : List AddExpr)).pretty (width := 0)
3.7.2.2. Atomic Types🔗
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.
🔗type classReprAtom.{u} (α : Type u) : Type
ReprAtom.{u} (α : Type u) : Type
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.
Instance Constructor
Atomic Types and Repr
All constructors of the inductive type ABC are without parameters:
inductive ABC where
| a
| b
| c
deriving Repr
The derived Repr ABC instance is used to display lists:
def abc : List ABC := [.a, .b, .c]
def abcs : List ABC := abc ++ abc ++ abc
[ABC.a,
ABC.b,
ABC.c,
ABC.a,
ABC.b,
ABC.c,
ABC.a,
ABC.b,
ABC.c]
#eval IO.println ((repr abcs).pretty (width := 14))
Because of the narrow width, line breaks are inserted:
This is because of the existence of a ReprAtom Nat instance.
Adding one for ABC leads to similar behavior:
instance : ReprAtom ABC := ⟨⟩
[ABC.a, ABC.b,
ABC.c, ABC.a,
ABC.b, ABC.c,
ABC.a, ABC.b,
ABC.c]
#eval IO.println ((repr abcs).pretty (width := 14))
