翻译规范 #1
Description
翻译原则可参考 Agda/Idris 文档翻译规范。
段落翻译
翻译通常以段落为基本单位。译者将原文围在 <!-- 和 --> 之间注释掉后，在下方空一行再进行翻译。考虑到中文斜体的渲染问题，英文原文中出现的 _text_ 在翻译时需改为 **文本**，特殊格式需要在两侧留下空格以便正确解析。例如：
<!--
Now that we've defined the naturals and operations upon them, our next
step is to learn how to prove properties that they satisfy. As hinted
by their name, properties of _inductive datatypes_ are proved by
_induction_.
-->
现在我们定义了自然数及其运算，下一步是学习如何证明它们满足的性质。
如其名称所示，**归纳数据类型（inductive datatype）**是通过**归纳（induction）**
来证明的。
术语翻译
文档中的术语请参考术语表，术语在正文中第一次出现时，如果是名词，需要在后面的括号中注明英文原词，首字母大写；如果不是名词，则为小写；标题中不添加英文。常见术语一般无需添加原词。示例见上。
标点符号
为了排版美观，中文和英文、数字之间要留有空格，中文标点和英文、数字之间无需空格。例如：
<!--
We require equality as in the previous chapter, plus the naturals
and some operations upon them. We also import a couple of new operations,
`cong`, `sym`, and `_≡⟨_⟩_`, which are explained below:
-->
我们需要上一章中的相等性，加上自然数及其运算。我们还导入了一些新的运算：
`cong`、`sym` 和 `_≡⟨_⟩_`，之后会解释它们：
列表翻译
为了让源码中的上下文更加紧凑，较短的列表一般整块注释掉后再在下方翻译；如果列表前的段落不长且后跟冒号，则可一并注释。例如：
<!--
* _Identity_. Operator `+` has left identity `0` if `0 + n ≡ n`, and
right identity `0` if `n + 0 ≡ n`, for all `n`. A value that is both
a left and right identity is just called an identity. Identity is also
sometimes called _unit_.
* _Associativity_. Operator `+` is associative if the location
of parentheses does not matter: `(m + n) + p ≡ m + (n + p)`,
for all `m`, `n`, and `p`.
* _Commutativity_. Operator `+` is commutative if order of
arguments does not matter: `m + n ≡ n + m`, for all `m` and `n`.
* _Distributivity_. Operator `*` distributes over operator `+` from the
left if `(m + n) * p ≡ (m * p) + (n * p)`, for all `m`, `n`, and `p`,
and from the right if `m * (p + q) ≡ (m * p) + (m * q)`, for all `m`,
`p`, and `q`.
-->
* **幺元（Identity）**。对于所有的 `n`，若 `0 + n ≡ n`，则 `+` 有左幺元 `0`；
若 `n + 0 ≡ n`，则 `+` 有右幺元 `0`。同时为左幺元和右幺元的值称简称幺元。
幺元有时也称作**单位元（Unit）**。
* **结合律（Associativity）**。若括号的位置无关紧要，则称运算符 `+` 满足结合律，
即对于所有的 `m`、`n` 和 `p`，有 `(m + n) + p ≡ m + (n + p)`。
* **交换律（Commutativity）**。若参数的位置无关紧要，则称运算符 `+` 满足交换律，
即对于所有的 `m` 和 `n`，有 `m + n ≡ n + m`。
* **分配率（Distributivity）**。对于所有的 `m`、`n` 和 `p`，若
`(m + n) * p ≡ (m * p) + (n * p)`，则运算符 `*` 对运算符 `+` 满足左分配率；
对于所有的 `m`、`n` 和 `p`，若 `m * (p + q) ≡ (m * p) + (m * q)`，则满足右分配率。
代码块翻译
一般来说，代码块直接跳过不用翻译。不过有时代码块中包含需要翻译的注释，因此请整块注释掉后再进行翻译。例如：
<!--
```
-- Your code goes here
```
-->
```
-- 请将代码写在此处。
```