Programming, Proving, and Performance: translated

functional-programming-lean/po/zh-CN.po

@@ -20231,7 +20231,7 @@ msgid ""
 "When pattern matching refines the type of a program in addition to "
 "discovering the structure of a value, it is called _dependent pattern "
 "matching_."
-msgstr "当模式匹配除了发现值结构体之外还细化程序的类型时，它被称为 _依赖模式匹配_。"
+msgstr "当模式匹配除了发现值结构体之外还细化程序的类型时，它被称为 _依值模式匹配_。"
 
 #: src/dependent-types/indexed-families.md:113
 #, fuzzy
@@ -20554,7 +20554,7 @@ msgid ""
 "`NatOrBool.bool.asType`, and these compute to the actual types `Nat` and "
 "`Bool`."
 msgstr ""
-"对 `t` 进行依赖模式匹配可以分别将预期结果类型 `t.asType` 优化为 `NatOrBool.nat.asType` 和 "
+"对 `t` 进行依值模式匹配可以分别将预期结果类型 `t.asType` 优化为 `NatOrBool.nat.asType` 和 "
 "`NatOrBool.bool.asType`，它们计算为实际类型 `Nat` 和 `Bool`。"
 
 #: src/dependent-types/universe-pattern.md:40
@@ -21081,7 +21081,7 @@ msgid ""
 "the `Repr` instances for `Int`, `String`, and `Bool` to be used:"
 msgstr ""
 "可以使用相同技术编写 `Repr` 实例。`Repr` 类的函数被称为 "
-"`reprPrec`，因为它旨在在显示值时考虑运算符优先级等因素。通过依赖模式匹配细化类型，可以使用 `Int`、`String` 和 `Bool` 的"
+"`reprPrec`，因为它旨在在显示值时考虑运算符优先级等因素。通过依值模式匹配细化类型，可以使用 `Int`、`String` 和 `Bool` 的"
 " `Repr` 实例中的 `reprPrec` 函数："
 
 #: src/dependent-types/typed-queries.md:81
@@ -23656,7 +23656,7 @@ msgstr ""
 "在策略语言中，可以有多个目标。每个目标由一个类型和一些假设组成。这些类似于使用下划线作为占位符——目标中的类型表示要证明的内容，而假设表示范围内可以使用的内容。在目标"
 " `case zero` 的情况下，没有假设，类型为 `Nat.zero = Nat.plusR 0 Nat.zero`——这是定理陈述，其中 `0` "
 "代替了 `k`。在目标 `case succ` 中，有两个假设，分别命名为 `n✝` 和 `n_ih✝`。在幕后，`induction` "
-"策略创建了一个依赖模式匹配，它细化了整体类型，`n✝` 表示模式中 `Nat.succ` 的参数。假设 `n_ih✝` 表示在 `n✝` "
+"策略创建了一个依值模式匹配，它细化了整体类型，`n✝` 表示模式中 `Nat.succ` 的参数。假设 `n_ih✝` 表示在 `n✝` "
 "上递归调用生成函数的结果。它的类型是定理的整体类型，只是用 `n✝` 代替了 `k`。作为目标 `case succ` "
 "的一部分要实现的类型是整体定理陈述，其中 `Nat.succ n✝` 代替了 `k`。"
 
@@ -24534,7 +24534,7 @@ msgstr ""
 "`rfl` 策略无法在此处应用，因为 `NonTail.sum` 和 `Tail.sum` "
 "在定义上不相等。然而，函数可以以不止定义相等的方式相等。还可以通过证明两个函数对相同输入产生相等输出，来证明它们相等。换句话说，\\\\( f = g "
 "\\\\) 可以通过证明 \\\\( f(x) = g(x) \\\\) 对于所有可能的输入 \\\\( x \\\\) 来证明。此原理称为 "
-"_函数扩展性_。函数扩展性正是 `NonTail.sum` 等于 `Tail.sum` 的原因：它们都对数字列表求和。"
+"_函数外延性_。函数外延性正是 `NonTail.sum` 等于 `Tail.sum` 的原因：它们都对数字列表求和。"
 
 #: src/programs-proofs/tail-recursion-proofs.md:27
 #, fuzzy
@@ -24546,7 +24546,7 @@ msgid ""
 "equal:"
 msgstr ""
 "在 Lean 的策略语言中，使用 `funext` "
-"调用函数扩展性，后跟一个用于任意参数的名称。任意参数作为假设添加到上下文中，目标变为要求证明应用于此参数的函数相等："
+"调用函数外延性，后跟一个用于任意参数的名称。任意参数作为假设添加到上下文中，目标变为要求证明应用于此参数的函数相等："
 
 #: src/programs-proofs/tail-recursion-proofs.md:40
 #, fuzzy
@@ -24830,7 +24830,7 @@ msgid ""
 "The actual proof requires only a little additional work to get the goal to "
 "match the helper's type. The first step is still to invoke function "
 "extensionality:"
-msgstr "实际证明只需要一些额外的工作即可使目标与辅助类型的匹配。第一步仍然是调用函数扩展性："
+msgstr "实际证明只需要一些额外的工作即可使目标与辅助类型的匹配。第一步仍然是调用函数外延性："
 
 #: src/programs-proofs/tail-recursion-proofs.md:415
 #, fuzzy
@@ -25159,8 +25159,8 @@ msgid ""
 "dependent pattern matching is `cases`, which has a syntax similar to that of"
 " `induction`:"
 msgstr ""
-"此错误发生是因为 `n + 2` 与 `5` 在定义上不相等。在普通的函数定义中，可以对假设 `three` 使用依赖模式匹配来将 `n` 细化为 "
-"`3`。`cases` 是依赖模式匹配的策略等价物，其语法类似于 `induction`："
+"此错误发生是因为 `n + 2` 与 `5` 在定义上不相等。在普通的函数定义中，可以对假设 `three` 使用依值模式匹配来将 `n` 细化为 "
+"`3`。`cases` 是依值模式匹配的策略等价物，其语法类似于 `induction`："
 
 #: src/programs-proofs/arrays-termination.md:136
 #, fuzzy
@@ -25926,7 +25926,7 @@ msgid ""
 "programs. Because `lst` has at least two entries, they can be exposed with "
 "`match`, which also refines the type through dependent pattern matching:"
 msgstr ""
-"模式匹配在策略脚本中与在程序中一样有效。因为`lst`至少有两个条目，所以它们可以用`match`暴露出来，它还通过依赖模式匹配来细化类型："
+"模式匹配在策略脚本中与在程序中一样有效。因为`lst`至少有两个条目，所以它们可以用`match`暴露出来，它还通过依值模式匹配来细化类型："
 
 #: src/programs-proofs/inequalities.md:509
 #, fuzzy
@@ -27510,7 +27510,7 @@ msgid ""
 "statement that relates arbitrary initial accumulator values to the final "
 "result of the original function is needed."
 msgstr ""
-"通常，证明两个函数相等是使用函数扩展性（`funext` "
+"通常，证明两个函数相等是使用函数外延性（`funext` "
 "策略）完成的，即如果两个函数对每个输入返回相同的值，则它们相等。如果函数是递归的，那么归纳通常是证明其输出相同的好方法。通常，函数的递归定义将对一个特定参数进行递归调用；这个参数是归纳的一个好选择。在某些情况下，归纳假设不够充分。解决这个问题通常需要考虑如何构建定理陈述的更通用版本，以提供足够充分的归纳假设。特别是，为了证明一个函数等价于一个累加器传递版本，需要一个将任意初始累加器值与原始函数的最终结果联系起来的定理陈述。"
 
 #: src/programs-proofs/summary.md:46

functional-programming-lean/src/SUMMARY.md

@@ -63,11 +63,11 @@
 - [编程、证明与性能](programs-proofs.md)
   - [尾递归](programs-proofs/tail-recursion.md)
   - [证明等价](programs-proofs/tail-recursion-proofs.md)
-  - [数组与停机](programs-proofs/arrays-termination.md)
+  - [数组与停机性](programs-proofs/arrays-termination.md)
   - [更多不等式](programs-proofs/inequalities.md)
   - [安全数组索引](programs-proofs/fin.md)
   - [插入排序与数组可变性](programs-proofs/insertion-sort.md)
   - [特殊类型](programs-proofs/special-types.md)
   - [总结](programs-proofs/summary.md)
 
-[接下来做什么](next-steps.md)
+[下一步](next-steps.md)

functional-programming-lean/src/getting-to-know/conveniences.md

@@ -870,15 +870,15 @@ Adding an annotation, such as in `{{#example_in Examples/Intro.lean pointPosWith
 ## String Interpolation
 -->
 
-## 字符串内插
+## 字符串插值
 
 <!--
 In Lean, prefixing a string with `s!` triggers _interpolation_, where expressions contained in curly braces inside the string are replaced with their values.
 This is similar to `f`-strings in Python and `$`-prefixed strings in C#.
 For instance,
 -->
 
-在 Lean 中，在字符串前加上 `s!` 会触发 **内插（Interpolation）** ，
+在 Lean 中，在字符串前加上 `s!` 会触发 **插值（Interpolation）** ，
 其中字符串中大括号内的表达式会被其值替换。这类似于 Python 中的 `f` 字符串和
 C# 中以 `$` 为前缀的字符串。例如，
 
@@ -901,7 +901,7 @@ Not all expressions can be interpolated into a string.
 For instance, attempting to interpolate a function results in an error.
 -->
 
-并非所有的表达式都可以内插到字符串中。例如，尝试内插一个函数会产生错误。
+并非所有的表达式都可以插值到字符串中。例如，尝试插值一个函数会产生错误。
 
 ```lean
 {{#example_in Examples/Intro.lean interpolationOops}}

functional-programming-lean/src/getting-to-know/datatypes-and-patterns.md

@@ -486,5 +486,5 @@ This topic is explored in [the final chapter](../programs-proofs/inequalities.md
 -->
 
 此消息表示 `div` 需要手动证明停机。这个主题在
-[最后一章](../programs-proofs/inequalities.md#division-as-iterated-subtraction)
+[最后一章](../programs-proofs/inequalities.md#用减法迭代表示除法)
 中进行了探讨。

functional-programming-lean/src/hello-world/running-a-program.md

@@ -349,5 +349,5 @@ Finally, the last line in the program is:
 It uses [string interpolation](../getting-to-know/conveniences.md#string-interpolation) to insert the provided name into a greeting string, writing the result to `stdout`.
 -->
 
-它使用[字符串内插](../getting-to-know/conveniences.md#string-interpolation)
+它使用[字符串插值](../getting-to-know/conveniences.md#字符串插值)
 将提供的名称插入到问候字符串中，并将结果写入到 `stdout`。

functional-programming-lean/src/hello-world/step-by-step.md

@@ -86,7 +86,7 @@ Statements that consist only of expressions do not introduce any new variables.
 该代码块中的第一个语句 `{{#include ../../../examples/hello-name/HelloName.lean:line3}}`
 由一个表达式组成。要执行一个表达式，首先要对其进行求值。在这种情况下，`IO.FS.Stream.putStrLn`
 的类型为 `IO.FS.Stream → String → IO Unit`。这意味着它是一个接受流和字符串并返回 `IO` 活动的函数。
-该表达式使用[访问器记法](../getting-to-know/structures.md#behind-the-scenes)进行函数调用。
+该表达式使用[访问器记法](../getting-to-know/structures.md#幕后)进行函数调用。
 此函数应用于两个参数：标准输出流和字符串。表达式的值为一个 `IO` 活动，
 该活动将字符串和换行符写入输出流。得到此值后，下一步是执行它，这会导致字符串和换行符写入到
 `stdout`。仅由表达式组成的语句不会引入任何新变量。