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: In the application
  Nat.succ "two"
the argument
  "two"
has type
  String : Type
but is expected to have type
  Nat : Type

策略证明的状态通常通过可点击的小按钮指示，例如在rfl之后:

(译者注: 注意by和rfl之后有一个很小的长条状按钮，或者当鼠标移动到by或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. 常量、语法和策略参考🔗

定义、归纳类型、语法生成器和战术有特定的描述。这些描述标记如下：

Even : Nat → Prop
Even : Nat → Prop

zero : Even 0

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