The Lean Language Reference

3. Interacting with Lean🔗

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

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

3.1. Evaluating Terms🔗

The Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval command is used to run code as a program. In particular, it is capable of executing IO actions, it uses a call-by-value evaluation strategy, partial functions are executed, and both types and proofs are erased. Use Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions. #reduce to instead reduce terms using the reduction rules that are part of definitional equality.

syntaxEvaluating Terms
command ::= ...
    | `#eval e` evaluates the expression `e` by compiling and evaluating it.

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

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

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

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

See also: `#reduce e` for evaluation by term reduction.
#eval term
command ::= ...
    | `#eval e` evaluates the expression `e` by compiling and evaluating it.

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

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

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

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

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

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

  • The command attempts to use ToExpr, Repr, or ToString instances to print the result.

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

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

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

Options:

  • If eval.pp is true (default: true) then tries to use ToExpr instances to make use of the usual pretty printer. Otherwise, only tries using Repr and ToString instances.

  • If eval.type is true (default: false) then pretty prints the type of the evaluated value.

  • If eval.derive.repr is true (default: true) then attempts to auto-derive a Repr instance when there is no other way to print the result.

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

Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval always elaborates and compiles the provided term. It then checks whether the term transitively depends on any uses of sorry, in which case evaluation is terminated unless the command was invoked as Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval!. This is because compiled code may rely on compile-time invariants (such as array lookups being in-bounds) that are ensured by proofs of suitable statements, and running code that contains incomplete proofs (or uses of sorry that “prove” incorrect statements) can cause Lean itself to crash.

The way the code is run depends on its type:

  • If the type is in the IO monad, then it is executed in a context where standard output and standard error are captured and redirected to the Lean message log. If the returned value's type is not Unit, then it is displayed as if it were the result of a non-monadic expression.

  • If the type is in one of the internal Lean metaprogramming monads (CommandElabM, TermElabM, MetaM, or CoreM), then it is run in the current context. For example, the environment will contain the definitions that are in scope where Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval is invoked. As with IO, the resulting value is displayed as if it were the result of a non-monadic expression. When Lean is running under Lake, its working directory (and thus the working directory for IO actions) is the current workspace.

  • If the type is in some other monad m, and there is a MonadLiftT m CommandElabM or MonadEvalT m CommandElabM instance, then MonadLiftT.monadLift or MonadEvalT.monadEval is used to transform the monad into one that may be run with Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval, after which it is run as usual.

  • If the term's type is not in any of the supported monads, then it is treated as a pure value. The compiled code is run, and the result is displayed.

Auxiliary definitions or other environment modifications that result from elaborating the term in Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval are discarded. If the term is an action in a metaprogramming monad, then changes made to the environment by 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 
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
Live ↪
🔗option
eval.pp

Default value: true

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

🔗option
eval.type

Default value: false

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

🔗option
eval.derive.repr

Default value: true

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

Monads can be given the ability to execute in Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval by defining a suitable MonadLiftMonadLift is described in the section on lifting monads. or MonadEval instance. Just as MonadLiftT is the transitive closure of MonadLift instances, MonadEvalT is the transitive closure of MonadEval instances. As with MonadLiftT users should not define additional instances of MonadEvalT directly.

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

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

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

Instance Constructor

MonadEval.mk.{u, v, w}

Methods

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

Evaluates a value from monad m into monad n.

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

The transitive closure of MonadEval.

Instance Constructor

MonadEvalT.mk.{u, v, w}

Methods

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

Evaluates a value from monad m into monad n.

3.2. Reducing Terms🔗

The Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions. #reduce command repeatedly applies reductions to a term until no further reductions are possible. Reductions are performed under binders, but to avoid unexpected slowdowns, proofs and types are skipped unless the corresponding options to Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions. #reduce are enabled. Unlike Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval command, reduction cannot have side effects and the result is displayed as a term rather than via a ToString or Repr instance.

Generally speaking, Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions. #reduce is primarily useful for diagnosing issues with definitional equality and proof terms, while Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval is more suitable for computing the value of a term. In particular, functions defined using well-founded recursion or as partial fixpoints are either very slow to compute with the reduction engine, or will not reduce at all.

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

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

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

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

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

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

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

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

Reducing Functions

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

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

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

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

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

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.4 → List ?m.4#check fun x => [x] 
fun x => [x] : ?m.4 → List ?m.4

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.7) → ?m.8 x#check fun x => x + x 
fun x => x + x : (x : ?m.7) → ?m.8 x
Live ↪
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.5#check_failure failed to synthesize instance of type class HAdd String Nat ?m.5 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command."one" + 1 
failed to synthesize instance of type class
  HAdd String Nat ?m.5

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Nonetheless, a partially-elaborated term is available:

"one" + 1 : ?m.5
Live ↪

3.4. Synthesizing Instances🔗

syntaxSynthesizing Instances
command ::= ...
    | #synth term

The Lean.Parser.Command.synth : command#synth command invokes Lean's type class resolution machinery and attempts to perform instance synthesis to find an instance for the given type class. If it succeeds, then the resulting instance term is output.

Synthesizing a Type Class Instance

Lean uses type classes to overload operations like addition. The + operator is notation for a call to HAdd.hAdd, which is the single method in the HAdd type class. This example shows that Lean will let us add two integers, and the result will be an integer:

instHAdd#synth HAdd Int Int Int 
instHAdd

By default, Lean does not show the implicit arguments in the output term. Instance arguments are implicit, however, which decreases the usefulness of this output for understanding instance synthesis. Setting the option pp.explicit to true causes Lean to display implicit arguments, including instances:

set_option pp.explicit true in @instHAdd Int Int.instAdd#synth HAdd Int Int Int 
@instHAdd Int Int.instAdd

Lean does not allow the addition of integers and strings, as demonstrated by this failure of type class instance synthesis:

failed to synthesize HAdd Int String String Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.#synth HAdd Int String String 
failed to synthesize
  HAdd Int String String

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

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. See the documentation for axioms for more information.

Printing Axioms

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

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

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

theorem swap_eq_swap' : swap = swap' := ⊢ swap = swap' x:BitVec 32y:BitVec 32⊢ swap x y = swap' x y x:BitVec 32y:BitVec 32⊢ y = x ^^^ y ^^^ (x ^^^ y ^^^ y) ∧ x = x ^^^ y ^^^ y All goals completed! 🐙

The resulting proof makes use of a number of axioms:

'swap_eq_swap'' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]#print axioms swap_eq_swap' 
'swap_eq_swap'' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]
Live ↪
syntaxPrinting Equations

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

command ::= ...
    | #print equations ident
command ::= ...
    | #print eqns ident
Printing Equations
def intersperse (x : α) : List α → List α | y :: z :: zs => y :: x :: intersperse x (z :: zs) | xs => xs equations: @[defeq] theorem intersperse.eq_1.{u_1} : ∀ {α : Type u_1} (x y z : α) (zs : List α), intersperse x (y :: z :: zs) = y :: x :: intersperse x (z :: zs) theorem intersperse.eq_2.{u_1} : ∀ {α : Type u_1} (x : α) (x_1 : List α), (∀ (y z : α) (zs : List α), x_1 = y :: z :: zs → False) → intersperse x x_1 = x_1#print equations intersperse 
equations:
@[defeq] theorem intersperse.eq_1.{u_1} : ∀ {α : Type u_1} (x y z : α) (zs : List α),
  intersperse x (y :: z :: zs) = y :: x :: intersperse x (z :: zs)
theorem intersperse.eq_2.{u_1} : ∀ {α : Type u_1} (x : α) (x_1 : List α),
  (∀ (y z : α) (zs : List α), x_1 = y :: z :: zs → False) → intersperse x x_1 = x_1

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

intersperse.eq_def.{u_1} {α : Type u_1} (x : α) (x✝ : List α) : intersperse x x✝ = match x✝ with | y :: z :: zs => y :: x :: intersperse x (z :: zs) | xs => xs#check intersperse.eq_def 
intersperse.eq_def.{u_1} {α : Type u_1} (x : α) (x✝ : List α) :
  intersperse x x✝ =
    match x✝ with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs
intersperse.eq_unfold.{u_1} : @intersperse = fun {α} x x_1 => match x_1 with | y :: z :: zs => y :: x :: intersperse x (z :: zs) | xs => xs#check intersperse.eq_unfold 
intersperse.eq_unfold.{u_1} :
  @intersperse = fun {α} x x_1 =>
    match x_1 with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs
Live ↪
syntaxScope Information

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

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

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

section open Nat namespace A variable (n : Nat) namespace B open List set_option pp.funBinderTypes true namespace A.B open Nat List variable (n : Nat) set_option pp.tagAppFns true set_option pp.funBinderTypes true#where end A.B end 
namespace A.B

open Nat List

variable (n : Nat)

set_option pp.tagAppFns true
set_option pp.funBinderTypes true
Live ↪
syntaxChecking the Lean Version

Shows the current Lean version. Prints Lean.versionString.

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

3.6. Testing Output with #guard_msgs🔗

The Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors 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, positions := false)`.

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.

Position reporting:
- `positions := true` reports the ranges of all messages relative to the line on which
  `#guard_msgs` appears.
- `positions := false` does not report position info.

For example, `#guard_msgs (error, drop all) in cmd` means to check errors 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.

At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
`plainDocComment` to always treat the contents as plain text.

A plain text doc comment 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.
A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
docComment?
      #guard_msgs ((guardMsgsSpecElt,*))? in
      command

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

Basic example:

/-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x

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

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

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

or only errors

#guard_msgs(error) in declaration uses 'sorry'example : α := sorry

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

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

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

#guard_msgs (

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

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.

Position reporting:

  • positions := true reports the ranges of all messages relative to the line on which #guard_msgs appears.

  • positions := false does not report position info.

For example, #guard_msgs (error, drop all) in cmd means to check errors 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, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors 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 /-- info: [] -/ #guard_msgs in #eval reverse ([] : List Nat) /-- info: ['c', 'b', 'a'] -/ #guard_msgs in #eval reverse "abc".toList
Live ↪

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, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors 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:

  1. Providing a filter that selects a subset of messages to be checked

  2. Specifying a whitespace comparison strategy

  3. Deciding to sort messages by their content or by the order in which they were produced

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

syntaxSpecifying #guard_msgs Behavior
guardMsgsSpecElt ::=
    A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter
guardMsgsSpecElt ::= ...
    | Whitespace handling for `#guard_msgs`:
- `whitespace := exact` requires an exact whitespace match.
- `whitespace := normalized` converts all newline characters to a space before matching
  (the default). This allows breaking long lines.
- `whitespace := lax` collapses whitespace to a single space before matching.
In all cases, leading and trailing whitespace is trimmed before matching.
whitespace := guardMsgsWhitespaceArg
guardMsgsSpecElt ::= ...
    | Message ordering for `#guard_msgs`:
- `ordering := exact` uses the exact ordering of the messages (the default).
- `ordering := sorted` sorts the messages in lexicographic order.
  This helps with testing commands that are non-deterministic in their ordering.
ordering := guardMsgsOrderingArg

There are three kinds of options for Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present. #guard_msgs: filters, whitespace comparison strategies, and orderings.

syntaxOutput Filters for #guard_msgs
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter ::=
    A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
drop? all
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter ::= ...
    | A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
drop? info
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter ::= ...
    | A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
drop? warning
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsFilter ::= ...
    | A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
drop? error

A message filter specification for #guard_msgs.

  • info, warning, error: capture (non-trace) messages with the given severity level.

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

syntaxWhitespace Comparison for #guard_msgs
guardMsgsWhitespaceArg ::=
    exact
guardMsgsWhitespaceArg ::= ...
    | lax
guardMsgsWhitespaceArg ::= ...
    | normalized

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

  • whitespace := exact requires an exact whitespace match.

  • whitespace := normalized converts all newline characters to a space before matching (the default). This allows breaking long lines.

  • whitespace := lax collapses whitespace to a single space before matching.

The option guard_msgs.diff controls the content of the error message that Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present. #guard_msgs produces when the expected message doesn't match the produced message. By default, Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present. #guard_msgs shows a line-by-line difference, with a leading + used to indicate lines from the produced message and a leading - used to indicate lines from the expected message. When messages are large and only differ by a small amount, this can make it easier to notice where they differ. Setting guard_msgs.diff to false causes Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present. #guard_msgs to instead show just the produced message, which can be compared with the expected message in the source file. This can be convenient if the difference between the message is confusing or overwhelming.

🔗option
guard_msgs.diff

Default value: true

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, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors 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 < 5 then .branches [.val n, .val (n - 1), .val n, .val (n - 2)] 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:

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

The evaluation produces:

Tree.branches
  [Tree.branches
     [Tree.branches
        [Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
         Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
      Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
   Tree.branches
     [Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
      Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]

Without guard_msgs.diff, the Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. 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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. For example, `#guard_msgs (error, drop all) in cmd` means to check errors 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.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
         Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
      Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
   Tree.branches
     [Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
      Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]

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

set_option guard_msgs.diff true in /-- info: Tree.branches [Tree.branches [Tree.branches [Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0], Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0, Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]], Tree.branches [Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1], Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]] -/ ❌️ Docstring on `#guard_msgs` does not match generated message: info: Tree.branches [Tree.branches [Tree.branches [Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0], - Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0, + Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]], Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]], Tree.branches [Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1], Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]] #guard_msgs in Tree.branches [Tree.branches [Tree.branches [Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0], Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]], Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]], Tree.branches [Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1], Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, 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.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
-          Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0,
+          Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
        Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
     Tree.branches
       [Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
        Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]
Live ↪

3.7. Formatted Output🔗

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:

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

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

3.7.1. Format🔗

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 
( 1 2 3 4 5 )

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)) 
(
  1
  2
  3
  4
  5
)

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 
( ( 1 2 3 4 5 ) ( 1 2 3 4 5 ) ( 1 2 3 4 5 ) )

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)) 
(
  ( 1 2 3 4 5 )
  ( 1 2 3 4 5 )
  ( 1 2 3 4 5 )
)

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)) 
(
  (
    1
    2
    3
    4
    5
  )
  (
    1
    2
    3
    4
    5
  )
  (
    1
    2
    3
    4
    5
  )
)
Live ↪
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 )
( 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) 
( 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 )

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) 
(
  1
  2
  3
  4
  5
  6
  7
  8
  9
  10
  11
  12
  13
  14
  15
  16
  17
  18
  19
  20
)

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) 
( 1 2 3 4 5 6 7 8 9 10 11 12
  13 14 15 16 17 18 19 20 )

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))) 
( 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 )
Live ↪
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"

Printing the string both with and without grouping results in the newlines being used:

abc xyz 123 #eval IO.println str.pretty 
abc
xyz
123
abc xyz 123 #eval IO.println (group str).pretty 
abc
xyz
123

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 
abc
xyz
123abc
xyz
123

Increasing the indentation level, however, causes all three lines of the string to begin at the same column:

It is: abc xyz 123 #eval IO.println (text "It is:" ++ indentD str).pretty 
It is:
  abc
  xyz
  123
It is: abc xyz 123 #eval IO.println (nest 8 <| text "It is:" ++ align true ++ str).pretty 
It is:  abc
        xyz
        123
Live ↪

3.7.1.1. Documents🔗

🔗inductive type
Std.Format : Type
Std.Format : Type

A representation of a set of strings, in which the placement of newlines and indentation differ.

Given a specific line width, specified in columns, the string that uses the fewest lines can be selected.

The pretty-printing algorithm is based on Wadler's paper A Prettier Printer.

Constructors

nil : Std.Format

The empty format.

line : Std.Format

A position where a newline may be inserted if the current group does not fit within the allotted column width.

align (force : Bool) : Std.Format

align tells the formatter to pad with spaces to the current indentation level, or else add a newline if we are already at or past the indent.

If force is true, then it will pad to the indent even if it is in a flattened group.

Example:

open Std Format in
#eval IO.println (nest 2 <| "." ++ align ++ "a" ++ line ++ "b")
. a b
text : String → Std.Format

A node containing a plain string.

If the string contains newlines, the formatter emits them and then indents to the current level.

nest (indent : Int) (f : Std.Format) : Std.Format

nest indent f increases the current indentation level by indent while rendering f.

Example:

open Std Format in def fmtList (l : List Format) : Format := let f := joinSep l (", " ++ Format.line) group (nest 1 <| "[" ++ f ++ "]")

This will be written all on one line, but if the text is too large, the formatter will put in linebreaks after the commas and indent later lines by 1.

append : Std.Format → Std.Format → Std.Format

Concatenation of two Formats.

group :
  Std.Format →
    (behavior :
        optParam Std.Format.FlattenBehavior
          Std.Format.FlattenBehavior.allOrNone) →
      Std.Format

Creates a new flattening group for the given inner Format.

tag : Nat → Std.Format → Std.Format

Used for associating auxiliary information (e.g. Exprs) with Format objects.

🔗inductive type
Std.Format.FlattenBehavior : Type
Std.Format.FlattenBehavior : Type

Determines how groups should have linebreaks inserted when the text would overfill its remaining space.

  • allOrNone will make a linebreak on every Format.line in the group or none of them.

    [1, 2, 3]

  • fill will only make linebreaks on as few Format.lines as possible:

    [1, 2, 3]

Constructors

allOrNone : Std.Format.FlattenBehavior

Either all Format.lines in the group will be newlines, or all of them will be spaces.

fill : Std.Format.FlattenBehavior

As few Format.lines in the group as possible will be newlines.

🔗def
Std.Format.fill (f : Std.Format) : Std.Format
Std.Format.fill (f : Std.Format) :
  Std.Format

Creates a group in which as few Format.lines as possible are rendered as newlines.

This is an alias for Format.group, with FlattenBehavior set to fill.

3.7.1.2. Empty Documents🔗

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.

🔗def
Std.Format.isEmpty : Std.Format → Bool
Std.Format.isEmpty : Std.Format → Bool

Checks whether the given format contains no characters.

🔗def
Std.Format.isNil : Std.Format → Bool
Std.Format.isNil : Std.Format → Bool

Checks whether a Format is the constructor Format.nil.

This does not check whether the resulting rendered strings are always empty. To do that, use Format.isEmpty.

3.7.1.3. Sequences🔗

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

🔗def
Std.Format.join (xs : List Std.Format) : Std.Format
Std.Format.join (xs : List Std.Format) :
  Std.Format

Concatenates a list of Formats with ++.

🔗def
Std.Format.joinSep.{u} {α : Type u} [Std.ToFormat α] :
  List α → Std.Format → Std.Format
Std.Format.joinSep.{u} {α : Type u}
  [Std.ToFormat α] :
  List α → Std.Format → Std.Format

Intercalates the given list with the given sep format.

The list items are formatting using ToFormat.format.

🔗def
Std.Format.prefixJoin.{u} {α : Type u} [Std.ToFormat α]
  (pre : Std.Format) : List α → Std.Format
Std.Format.prefixJoin.{u} {α : Type u}
  [Std.ToFormat α] (pre : Std.Format) :
  List α → Std.Format

Concatenates the given list after prepending pre to each element.

The list items are formatting using ToFormat.format.

🔗def
Std.Format.joinSuffix.{u} {α : Type u} [Std.ToFormat α] :
  List α → Std.Format → Std.Format
Std.Format.joinSuffix.{u} {α : Type u}
  [Std.ToFormat α] :
  List α → Std.Format → Std.Format

Concatenates the given list after appending the given suffix to each element.

The list items are formatting using ToFormat.format.

3.7.1.4. Indentation🔗

These operators make it easier to achieve a consistent indentation style on top of Std.Format.nest.

🔗def
Std.Format.nestD (f : Std.Format) : Std.Format
Std.Format.nestD (f : Std.Format) :
  Std.Format

Increases the indentation level by the default amount.

🔗def
Std.Format.defIndent : Nat
Std.Format.defIndent : Nat

The default indentation level, which is two spaces.

🔗def
Std.Format.indentD (f : Std.Format) : Std.Format
Std.Format.indentD (f : Std.Format) :
  Std.Format

Insert a newline and then f, all nested by the default indent amount.

3.7.1.5. Brackets and Parentheses🔗

These operators make it easier to achieve a consistent parenthesization style.

🔗def
Std.Format.bracket (l : String) (f : Std.Format) (r : String) :
  Std.Format
Std.Format.bracket (l : String)
  (f : Std.Format) (r : String) :
  Std.Format

Creates a format l ++ f ++ r with a flattening group, nesting the contents by the length of l.

The group's FlattenBehavior is allOrNone; for fill use Std.Format.bracketFill.

🔗def
Std.Format.sbracket (f : Std.Format) : Std.Format
Std.Format.sbracket (f : Std.Format) :
  Std.Format

Creates the format "[" ++ f ++ "]" with a flattening group, nesting by one space.

sbracket is short for “square bracket”.

🔗def
Std.Format.paren (f : Std.Format) : Std.Format
Std.Format.paren (f : Std.Format) :
  Std.Format

Creates the format "(" ++ f ++ ")" with a flattening group, nesting by one space.

🔗def
Std.Format.bracketFill (l : String) (f : Std.Format) (r : String) :
  Std.Format
Std.Format.bracketFill (l : String)
  (f : Std.Format) (r : String) :
  Std.Format

Creates a format l ++ f ++ r with a flattening group, nesting the contents by the length of l.

The group's FlattenBehavior is fill; for allOrNone use Std.Format.bracketFill.

3.7.1.6. Rendering🔗

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.

🔗def
Std.Format.pretty (f : Std.Format) (width : Nat := Std.Format.defWidth)
  (indent column : Nat := 0) : String
Std.Format.pretty (f : Std.Format)
  (width : Nat := Std.Format.defWidth)
  (indent column : Nat := 0) : String

Renders a Format to a string.

  • width: the total width

  • indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)

  • column: begin the first line wrap column characters earlier than usual (this is useful when the output String will be printed starting at column)

🔗def
Std.Format.defWidth : Nat
Std.Format.defWidth : Nat

The default width of the targeted output, which is 120 columns.

🔗def
Std.Format.prettyM {m : Type → Type} (f : Std.Format) (w : Nat)
  (indent : Nat := 0) [Monad m] [Std.Format.MonadPrettyFormat m] :
  m Unit
Std.Format.prettyM {m : Type → Type}
  (f : Std.Format) (w : Nat)
  (indent : Nat := 0) [Monad m]
  [Std.Format.MonadPrettyFormat m] :
  m Unit

Renders a Format using effects in the monad m, using the methods of MonadPrettyFormat.

Each line is emitted as soon as it is rendered, rather than waiting for the entire document to be rendered.

  • w: the total width

  • indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)

🔗type class
Std.Format.MonadPrettyFormat (m : Type → Type) : Type
Std.Format.MonadPrettyFormat
  (m : Type → Type) : Type

A monad that can be used to incrementally render Format objects.

Instance Constructor

Std.Format.MonadPrettyFormat.mk

Methods

pushOutput : String → m Unit

Emits the string s.

pushNewline : Nat → m Unit

Emits a newline followed by indent columns of indentation.

currColumn : m Nat

Gets the current column at which the next string will be emitted.

startTag : Nat → m Unit

Starts a region tagged with tag.

endTags : Nat → m Unit

Exits the scope of count opened tags.

3.7.1.7. The ToFormat Class

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.

🔗type class
Std.ToFormat.{u} (α : Type u) : Type u
Std.ToFormat.{u} (α : Type u) : Type u

Specifies a “user-facing” way to convert from the type α to a Format object. There is no expectation that the resulting string is valid code.

The Repr class is similar, but the expectation is that instances produce valid Lean code.

Instance Constructor

Std.ToFormat.mk.{u}

Methods

format : α → Std.Format

Converts a value to a Format object, with no expectation that the resulting string is valid code.

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 class
Repr.{u} (α : Type u) : Type u
Repr.{u} (α : Type u) : Type u

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

Repr.mk.{u}

Methods

reprPrec : α → Nat → Std.Format

Turn a value of type α into a Format at a given precedence. The precedence value can be used to avoid parentheses if they are not necessary.

🔗def
repr.{u_1} {α : Type u_1} [Repr α] (a : α) : Std.Format
repr.{u_1} {α : Type u_1} [Repr α]
  (a : α) : Std.Format

Turns a into a Format using its Repr instance. The precedence level is initially set to 0.

🔗def
reprStr.{u_1} {α : Type u_1} [Repr α] (a : α) : String
reprStr.{u_1} {α : Type u_1} [Repr α]
  (a : α) : String

Turns a into a String using its Repr instance, rendering the Format at the default width of 120 columns.

The precedence level is initially set to 0.

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) 
(NatOrInt.nat (3))
(NatOrInt.int (5))
(NatOrInt.int (-5))

However, (NatOrInt.nat (3)) is not particularly idiomatic Lean, and redundant parentheses can make it difficult to read large expressions.

Live ↪

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.

🔗def
Repr.addAppParen (f : Std.Format) (prec : Nat) : Std.Format
Repr.addAppParen (f : Std.Format)
  (prec : Nat) : Std.Format

Adds parentheses to f if the precedence prec from the context is at least that of function application.

Together with reprArg, this can be used to correctly parenthesize function application syntax.

🔗def
reprArg.{u_1} {α : Type u_1} [Repr α] (a : α) : Std.Format
reprArg.{u_1} {α : Type u_1} [Repr α]
  (a : α) : Std.Format

Turns a into a Format using its Repr instance, with the precedence level set to that of function application.

Together with Repr.addAppParen, this can be used to correctly parenthesize function application syntax.

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.nat 5
N.NatOrInt.int 5 #eval IO.println (repr (NatOrInt.int 5)) 
N.NatOrInt.int 5
N.NatOrInt.int (-5) #eval IO.println (repr (NatOrInt.int (-5))) 
N.NatOrInt.int (-5)
some (N.NatOrInt.int (-5)) #eval IO.println (repr (some (NatOrInt.int (-5)))) 
some (N.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]
[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 
[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]
Live ↪
Infix Syntax

This example demonstrates the use of precedences to encode a left-associative pretty printer. The type AddExpr represents expressions with constants and addition:

inductive AddExpr where | nat : Nat → AddExpr | add : AddExpr → AddExpr → AddExpr

The OfNat and Add instances provide a more convenient syntax for AddExpr:

instance : OfNat AddExpr n where ofNat := .nat n instance : Add AddExpr where add := .add

The Repr AddExpr instance should insert only the necessary parentheses. Lean's addition operator is left-associative, with precedence 65, so the recursive call to the left uses precedence 64 and the operator itself is parenthesized if the current context has precedence greater than or equal to 65:

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⟩

Regardless of the input's parenthesization, this instance inserts only the necessary parentheses:

2 + 3 + 4 #eval IO.println (repr (((2 + 3) + 4) : AddExpr)) 
2 + 3 + 4
2 + 3 + 4 #eval IO.println (repr ((2 + 3 + 4) : AddExpr)) 
2 + 3 + 4
2 + (3 + 4) #eval IO.println (repr ((2 + (3 + 4)) : AddExpr)) 
2 + (3 + 4)
[2 + (3 + 4), 2 + 3 + 4] #eval IO.println (repr ([2 + (3 + 4), (2 + 3) + 4] : List AddExpr)) 
[2 + (3 + 4), 2 + 3 + 4]

The uses of group, nestD, and line in the implementation lead to the expected newlines and indentation in a narrow context:

[2 + (3 + 4), 2 + 3 + 4] #eval ([2 + (3 + 4), (2 + 3) + 4] : List AddExpr) |> repr |>.pretty (width := 0) |> IO.println 
[2 +
   (3 +
      4),
 2 +
     3 +
   4]
Live ↪

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 class
ReprAtom.{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

ReprAtom.mk.{u}
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:

[ABC.a,
 ABC.b,
 ABC.c,
 ABC.a,
 ABC.b,
 ABC.c,
 ABC.a,
 ABC.b,
 ABC.c]

However, converting the list to a List Nat leads to a differently-formatted result.

def ABC.toNat : ABC → Nat | .a => 0 | .b => 1 | .c => 2 [0, 1, 2, 0, 1, 2, 0, 1, 2]#eval IO.print ((repr (abcs.map ABC.toNat)).pretty (width := 14))

There are far fewer line breaks:

[0, 1, 2, 0,
 1, 2, 0, 1,
 2]

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)) 
[ABC.a, ABC.b,
 ABC.c, ABC.a,
 ABC.b, ABC.c,
 ABC.a, ABC.b,
 ABC.c]
Live ↪