1.2.1. Lean 代码🔗

本文档包含许多 Lean 代码示例。 其格式如下：

编译器输出（可能是错误、警告，也可能只是信息）既会在代码中显示，也会单独显示：

信息性输出，例如 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 的结果，显示如下：

"The answer is 4"

警告显示如下：

declaration uses `sorry`

错误消息显示如下：

Application type mismatch: The argument
  "two"
has type
  String
but is expected to have type
  Nat
in the application
  Nat.succ "two"

tactic 证明状态由小菱形标记表示；点击该标记即可显示证明状态，例如下列 rfl 之后的标记：

证明状态也可以单独显示。 在试图证明 2 + 2 = 4 时，初始证明状态为：

使用 rflAll goals completed! 🐙 后，所得状态为：

代码示例中的标识符会超链接到其文档。

含语法错误的代码示例会标出解析错误发生的位置，并附上错误消息：

def f : Option Nat → Type  | some 0 => Unit  |unexpected token '=>'; expected term => Option (f t)  | none => Empty

<example>:3:3-3:6: unexpected token '=>'; expected term

1.2.2. 示例🔗

说明性示例置于提示框中，如下所示：

1.2.3. 技术术语🔗

技术术语 是指在撰写本参考手册这样的技术材料时，以非常特定的意义使用的词项。 技术术语的用例通常会像此处一样超链接到其定义位置。

1.2.4. 常量、语法与 tactic 参考🔗

定义、归纳类型、语法构造和 tactic 都有专门描述。 这些描述标记如下：

Even : Nat → Prop
Even : Nat → Prop

Even.zero : Even 0

Even.plusTwo {n : Nat} : Even n → Even (n + 2)