翻译规范

[OlingCat]

翻译原则可参考 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
```
-->

```
-- 请将代码写在此处。
```

[OlingCat]

如果你用 VSCode，那么可以安装我自用的一个简单扩展：
https://marketplace.visualstudio.com/items?itemName=OlingCat.trans-box
安装完成后在 VSCode 的配置里添加

    "trans.enclose": {
        "lagda.md": {
            "start": "<!--",
            "end": "-->"
        }
    }

然后光标放在想要翻译的段落中，按下 Alt-D，就会把当前段落注释掉，在下面复制一份。
例如：

This chapter introduces negation, and discusses intuitionistic
and classical logic.

然后把光标放到该段落中的任意位置，按下 Alt-D 后会变成：

<!--
This chapter introduces negation, and discusses intuitionistic
and classical logic.
-->

This chapter introduces negation, and discusses intuitionistic
and classical logic.

[fangyi-zhou]

在 plfa 的排版系统改成 Hakyll 过后，注释改成了 <!-- 和 -->。