fix bold

axioms_and_computation.md

@@ -59,8 +59,8 @@ computation. This also blocks evaluation in the kernel, but it is
 compatible with compilation to bytecode.
 -->
 
-Lean 的标准库定义了一个公理：**命题外延性（Propositional Extensionality）**。
-以及一个**商（Qoutient）**结构，它蕴含了函数外延性的公理。
+Lean 的标准库定义了一个公理： **命题外延性（Propositional Extensionality）** 。
+以及一个 **商（Qoutient）** 结构，它蕴含了函数外延性的公理。
 这些扩展被用来发展如集合与有限集这些理论。我们在后面会看到，
 这些定理的使用会阻碍 Lean 内核中的求值，因此 ``Nat`` 类型的封闭项不再求值为数值。
 但是 Lean 在对其虚拟机器求值器进行字节码编译时会擦除类型和命题信息，
@@ -163,7 +163,7 @@ computational reading.
 然而在 19 世纪，数学论证复杂性的提升推动了数学家发展新的推理风格，
 抑制算法信息并调用数学对象，从而抽象掉了对象被表征的细节。
 目标是在不陷入繁重的计算细节的情况下获得强大的「概念」理解，
-但这可能导致数学定理在直接计算的解读上干脆就是 **错误** 的。
+但这可能导致数学定理在直接计算的解读上干脆就是  **错误**  的。
 
 <!--
 There is still fairly uniform agreement today that computation is
@@ -183,9 +183,9 @@ mathematical reasoning.
 
 今天数学界仍在相当普遍地同意计算对于数学很重要。
 但对于如何以最佳方式解决计算问题有不同的看法。
-从**构造性**的角度来看，将数学与其计算根源分开是一个错误；
+从 **构造性** 的角度来看，将数学与其计算根源分开是一个错误；
 每条有意义的数学定理都应具有直接的计算解释。
-从**经典的**角度来看，保持关注点的分离更有成效：
+从 **经典的** 角度来看，保持关注点的分离更有成效：
 我们可以使用一种语言和方法体系编写计算机程序，
 同时保持使用非构造性理论和方法对其进行推理的自由。
 Lean 旨在支持这两种方法。库的核心部分以构造性方式开发，
@@ -516,8 +516,8 @@ quotients, and more. But the solutions are not so clear cut, and the
 rules of Lean's underlying calculus do not sanction such reductions.
 -->
 
-当前的研究计划包括关于**观测类型论（Observational Type Theory）**
-和**立方类型论（Cubical Type Theory）**的研究，旨在扩展类型理论，
+当前的研究计划包括关于 **观测类型论（Observational Type Theory）**
+和 **立方类型论（Cubical Type Theory）** 的研究，旨在扩展类型理论，
 以便允许对涉及函数外延、商，等等的强制转换进行归约。
 但解决方案并不明朗，而 Lean 的底层演算法则对此类归约也不支持。
 
@@ -724,7 +724,7 @@ was an equivalence relation to start with, then for all ``a`` and
 当然，当 ``r`` 是等价关系时，商集的结构是最常用的。给定上面的 ``r``，
 如果我们根据法则 ``r' a b`` 当且仅当 ``Quot.mk r a = Quot.mk r b`` 定义 ``r'``，
 那么显然 ``r'`` 就是一个等价关系。事实上，``r'`` 是函数 ``a ↦ quot.mk r a``
-的**核（Kernel）**。公理 ``Quot.sound`` 表明 ``r a b`` 蕴含 ``r' a b``。
+的 **核（Kernel）** 。公理 ``Quot.sound`` 表明 ``r a b`` 蕴含 ``r' a b``。
 使用 ``Quot.lift`` 和 ``Quot.ind``，我们可以证明 ``r'`` 是包含 ``r`` 的最小的等价关系，
 意思就是，如果 ``r''`` 是包含 ``r`` 的任意等价关系，则 ``r' a b`` 蕴含 ``r'' a b``。
 特别地，如果 ``r`` 开始就是一个等价关系，那么对任意 ``a`` 和 ``b``，我们都有
@@ -736,7 +736,7 @@ notion of a *setoid*, which is simply a type with an associated
 equivalence relation:
 -->
 
-为支持这种通用使用案例，标准库定义了 **广集（Setoid）** 的概念，
+为支持这种通用使用案例，标准库定义了  **广集（Setoid）**  的概念，
 它只是一个带有与之关联的等价关系的类型：
 
 ```lean
@@ -829,7 +829,7 @@ the relevant equivalence relation:
 -->
 
 回顾一下标准库中的 ``α × β`` 代表类型 ``α`` 和 ``β`` 的笛卡尔积。
-为了说明商的用法，让我们将类型为 ``α`` 的元素构成的**无序对（Unordered Pair）**的类型定义为
+为了说明商的用法，让我们将类型为 ``α`` 的元素构成的 **无序对（Unordered Pair）** 的类型定义为
 ``α × α`` 类型的商。首先，我们定义相关的等价关系：
 
 ```lean
@@ -1178,7 +1178,7 @@ subtypes as follows:
 -->
 
 这可以在 ``Classical`` 命名空间中找到，所以定理的全名是 ``Classical.choice``。
-选择公理等价于**非限定摹状词（Indefinite Description）**原理，可通过子类型表示如下：
+选择公理等价于 **非限定摹状词（Indefinite Description）** 原理，可通过子类型表示如下：
 
 ```lean
 # namespace Hidden
@@ -1254,7 +1254,7 @@ definition is conventionally known as *Hilbert's epsilon function*:
 -->
 
 假设环境类型 ``α`` 非空，``strongIndefiniteDescription p`` 产生一个满足 ``p``
-的元素 ``α``（如果存在的话）。该定义的数据部分通常被称为 **希尔伯特 ε 函数**：
+的元素 ``α``（如果存在的话）。该定义的数据部分通常被称为  **希尔伯特 ε 函数** ：
 
 ```lean
 # open Classical

dependent_type_theory.md

@@ -396,7 +396,7 @@ universes. For example, ``List α`` should make sense for any type
 type signature of the function ``List``:
 -->
 
-然而，有些操作需要在类型宇宙上具有**多态（Polymorphic）**。例如，``List α`` 应该对任何类型的 ``α`` 都有意义，无论 ``α`` 存在于哪种类型的宇宙中。所以函数 ``List`` 有如下的类型：
+然而，有些操作需要在类型宇宙上具有 **多态（Polymorphic）** 。例如，``List α`` 应该对任何类型的 ``α`` 都有意义，无论 ``α`` 存在于哪种类型的宇宙中。所以函数 ``List`` 有如下的类型：
 
 ```lean
 #check List    -- List.{u} (α : Type u) : Type u
@@ -488,7 +488,7 @@ any value ``x`` to the value ``t``.
 Here are some more examples
 -->
 
-从另一个表达式创建函数的过程称为**lambda 抽象**。假设你有一个变量 ``x : α`` 和一个表达式 ``t : β``，那么表达式 ``fun (x : α) => t`` 或者 ``λ (x : α) => t`` 是一个类型为 ``α → β`` 的对象。这个从 ``α`` 到 ``β`` 的函数把任意 ``x`` 映射到 ``t``。
+从另一个表达式创建函数的过程称为 **lambda 抽象** 。假设你有一个变量 ``x : α`` 和一个表达式 ``t : β``，那么表达式 ``fun (x : α) => t`` 或者 ``λ (x : α) => t`` 是一个类型为 ``α → β`` 的对象。这个从 ``α`` 到 ``β`` 的函数把任意 ``x`` 映射到 ``t``。
 
 这有些例子：
 
@@ -578,7 +578,7 @@ following expressions:
 
 这个表达式表示一个接受三个类型 ``α``，``β`` 和 ``γ`` 和两个函数 ``g : β → γ`` 和 ``f : α → β``，并返回的 ``g`` 和 ``f`` 的复合的函数。(理解这个函数的类型需要理解依值积类型，下面将对此进行解释。)
 
-lambda表达式的一般形式是 ``fun x : α => t``，其中变量 ``x`` 是一个**绑定变量（Bound Variable）**：它实际上是一个占位符，其「作用域」没有扩展到表达式 ``t`` 之外。例如，表达式 ``fun (b : β) (x : α) => b`` 中的变量 ``b`` 与前面声明的常量 ``b`` 没有任何关系。事实上，这个表达式表示的函数与 ``fun (u : β) (z : α) => u`` 是一样的。形式上，可以通过给绑定变量重命名来使形式相同的表达式被看作是**alpha等价**的，也就是被认为是「一样的」。Lean 认识这种等价性。
+lambda表达式的一般形式是 ``fun x : α => t``，其中变量 ``x`` 是一个 **绑定变量（Bound Variable）** ：它实际上是一个占位符，其「作用域」没有扩展到表达式 ``t`` 之外。例如，表达式 ``fun (b : β) (x : α) => b`` 中的变量 ``b`` 与前面声明的常量 ``b`` 没有任何关系。事实上，这个表达式表示的函数与 ``fun (u : β) (z : α) => u`` 是一样的。形式上，可以通过给绑定变量重命名来使形式相同的表达式被看作是 **alpha等价** 的，也就是被认为是「一样的」。Lean 认识这种等价性。
 
 注意到项 ``t : α → β`` 应用到项 ``s : α`` 上导出了表达式 ``t s : β``。回到前面的例子，为清晰起见给绑定变量重命名，注意以下表达式的类型:
 
@@ -1506,7 +1506,7 @@ used to specify the desired types of the expressions ``id`` and
 
 此处定义的 ``ident`` 和上面那个效果是一样的。
 
-Lean 有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些「洞」或「占位符」的过程通常被称为**繁饰（Elaboration）**。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 ``id`` 或 ``List.nil`` 这样的表达式被认为是「多态的」，因为它可以在不同的上下文中具有不同的含义。
+Lean 有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些「洞」或「占位符」的过程通常被称为 **繁饰（Elaboration）** 。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 ``id`` 或 ``List.nil`` 这样的表达式被认为是「多态的」，因为它可以在不同的上下文中具有不同的含义。
 
 可以通过写 ``(e : T)`` 来指定表达式 ``e`` 的类型 ``T``。这就指导 Lean 的繁饰器在试图解决隐式参数时使用值 ``T`` 作为 ``e`` 的类型。在下面的第二个例子中，这种机制用于指定表达式 ``id`` 和 ``List.nil`` 所需的类型:
 

induction_and_recursion.md

@@ -322,7 +322,7 @@ is a parameter and occurs before the colon to indicate it does not participate i
 Lean also allows parameters to occur after ``:``, but it cannot pattern match on them.
 -->
 
-还要注意的是，当定义中不需要一个参数的值时，你可以用下划线来代替。这个下划线被称为**通配符模式**，或**匿名变量**。与方程编译器之外的用法不同，这里的下划线**并不**表示一个隐参数。使用下划线表示通配符在函数式编程语言中是很常见的，所以 Lean 采用了这种符号。[通配符和重叠模式](#通配符和重叠模式)一节阐述了通配符的概念，而[不可访问模式](#不可访问模式)一节解释了你如何在模式中使用隐参数。
+还要注意的是，当定义中不需要一个参数的值时，你可以用下划线来代替。这个下划线被称为 **通配符模式** ，或 **匿名变量** 。与方程编译器之外的用法不同，这里的下划线 **并不** 表示一个隐参数。使用下划线表示通配符在函数式编程语言中是很常见的，所以 Lean 采用了这种符号。[通配符和重叠模式](#通配符和重叠模式)一节阐述了通配符的概念，而[不可访问模式](#不可访问模式)一节解释了你如何在模式中使用隐参数。
 
 正如[归纳类型](./inductive_types.md)一章中所描述的，归纳数据类型可以依赖于参数。下面的例子使用模式匹配定义了 ``tail`` 函数。参数 ``α : Type`` 是一个参数，出现在冒号之前，表示它不参与模式匹配。Lean 也允许参数出现在 ``:`` 之后，但它不能对其进行模式匹配。
 
@@ -350,7 +350,7 @@ considered in the [Section Dependent Pattern Matching](#dependent-pattern-matchi
 
 尽管参数 ``α`` 在这两个例子中的位置不同，但在这两种情况下，它的处理方式是一样的，即它不参与情况分割。
 
-Lean 也可以处理更复杂的模式匹配形式，其中从属类型的参数对各种情况构成了额外的约束。这种**依值模式匹配**的例子在[依值模式匹配](#依值模式匹配)一节中考虑。
+Lean 也可以处理更复杂的模式匹配形式，其中从属类型的参数对各种情况构成了额外的约束。这种 **依值模式匹配** 的例子在[依值模式匹配](#依值模式匹配)一节中考虑。
 
 <!--
 Wildcards and Overlapping Patterns
@@ -444,7 +444,7 @@ both approaches.
 
 你可以检查这个 ``foo`` 的定义是否满足与之前相同的定义特性。
 
-一些函数式编程语言支持**不完整的模式**。在这些语言中，解释器对不完整的情况产生一个异常或返回一个任意的值。我们可以使用 ``Inhabited`` （含元素的）类型类来模拟任意值的方法。粗略的说，``Inhabited α`` 的一个元素是对 ``α`` 拥有一个元素的见证；在[类型类](./type_classes.md)中，我们将看到 Lean 可以被告知合适的基础类型是含元素的，并且可以自动推断出其他构造类型是含元素的。在此基础上，标准库提供了一个任意元素 ``arbitrary``，任何含元素的类型。
+一些函数式编程语言支持 **不完整的模式** 。在这些语言中，解释器对不完整的情况产生一个异常或返回一个任意的值。我们可以使用 ``Inhabited`` （含元素的）类型类来模拟任意值的方法。粗略的说，``Inhabited α`` 的一个元素是对 ``α`` 拥有一个元素的见证；在[类型类](./type_classes.md)中，我们将看到 Lean 可以被告知合适的基础类型是含元素的，并且可以自动推断出其他构造类型是含元素的。在此基础上，标准库提供了一个任意元素 ``arbitrary``，任何含元素的类型。
 
 我们还可以使用类型`Option α`来模拟不完整的模式。我们的想法是对所提供的模式返回`some a`，而对不完整的情况使用`none`。下面的例子演示了这两种方法。
 
@@ -595,7 +595,7 @@ compiler:
 
 这里 `(a : α)` 是一个参数序列，`(b : β)` 是进行模式匹配的参数序列，`γ` 是任何类型，它可以取决于 `a` 和 `b `。每一行应该包含相同数量的模式，对应于 `β` 的每个元素。正如我们所看到的，模式要么是一个变量，要么是应用于其他模式的构造子，要么是一个正规化为该形式的表达式（其中非构造子用 ``[matchPattern]`` 属性标记）。构造子的出现会提示情况拆分，构造子的参数由给定的变量表示。在[依值模式匹配](#依值模式匹配)一节中，我们将看到有时有必要在模式中包含明确的项，这些项需要进行表达式类型检查，尽管它们在模式匹配中没有起到作用。由于这个原因，这些被称为「不可访问的模式」。但是在[依值模式匹配](#依值模式匹配)一节之前，我们将不需要使用这种不可访问的模式。
 
-正如我们在上一节所看到的，项 `t₁,...,tₙ` 可以利用任何一个参数 `a`，以及在相应模式中引入的任何一个变量。使得递归和归纳成为可能的是，它们也可以涉及对 ``foo`` 的递归调用。在本节中，我们将处理**结构性递归**，其中 `foo` 的参数出现在 `:=` 的右侧，是左侧模式的子项。我们的想法是，它们在结构上更小，因此在归纳类型中出现在更早的阶段。下面是上一章的一些结构递归的例子，现在用方程编译器来定义。
+正如我们在上一节所看到的，项 `t₁,...,tₙ` 可以利用任何一个参数 `a`，以及在相应模式中引入的任何一个变量。使得递归和归纳成为可能的是，它们也可以涉及对 ``foo`` 的递归调用。在本节中，我们将处理 **结构性递归** ，其中 `foo` 的参数出现在 `:=` 的右侧，是左侧模式的子项。我们的想法是，它们在结构上更小，因此在归纳类型中出现在更早的阶段。下面是上一章的一些结构递归的例子，现在用方程编译器来定义。
 
 ```lean
 open Nat
@@ -744,7 +744,7 @@ type. You can get a sense of how it works by looking at the types of
 
 在这两种情况下，Lean 都会生成辅助函数 ``fibFast.loop``。
 
-为了处理结构递归，方程编译器使用**值过程**（course-of-values）递归，使用由每个归纳定义类型自动生成的常量 `below` 和 `brecOn`。你可以通过查看 ``Nat.below`` 和 ``Nat.brecOn`` 的类型来了解它是如何工作的。
+为了处理结构递归，方程编译器使用 **值过程** （course-of-values）递归，使用由每个归纳定义类型自动生成的常量 `below` 和 `brecOn`。你可以通过查看 ``Nat.below`` 和 ``Nat.brecOn`` 的类型来了解它是如何工作的。
 
 ```lean
 variable (C : Nat → Type u)
@@ -1770,7 +1770,7 @@ implements a new feature, *discriminant refinement*, which includes
 these extra discriminants automatically for us.
 -->
 
-如前所述，参数 ``{n : Nat}`` 是模式匹配的一部分，因为它不能在整个定义中保持固定。在以前的 Lean 版本中，用户经常发现必须包含这些额外的判别符是很麻烦的。因此，Lean 4 实现了一个新特性，**判别精炼（discriminant refinement）**，它自动为我们包含了这些额外的判别。
+如前所述，参数 ``{n : Nat}`` 是模式匹配的一部分，因为它不能在整个定义中保持固定。在以前的 Lean 版本中，用户经常发现必须包含这些额外的判别符是很麻烦的。因此，Lean 4 实现了一个新特性， **判别精炼（discriminant refinement）** ，它自动为我们包含了这些额外的判别。
 
 ```lean
 # inductive Vector (α : Type u) : Nat → Type u