快速指南：Agda 代码的编辑、类型检查与编译¶

_quick-guide-introduction:

简介¶

Agda 程序通常使用 Emacs 或 Atom 来编辑。要编辑一个模块（假设你已经正确安装了 Agda 及其 Emacs 模式或 Atom插件），请启动编辑器并打开一个扩展名为 .agda 的文件。程序可以交互式地开发，这表示你可以对尚未完成的代码进行类型检查：如果用一个问号（?）作为表达式的占位符，然后检查缓冲区，那么 Agda 会将问号替换为一个「洞（hole）」，之后可以填充它。你还可以在洞的上下文中做一些其它的事情：列出上下文，推导表达式的类型，甚至可以对所涉及的变量在周围的上下文中被绑定的开项（open term）进行求值。

以下为最常用的命令（见 Notation for key combinations）：

C-c C-l: 加载。检查文件内容的类型。
C-c C-,: 显示目标的类型，即当前洞所预期的类型，以及局部定义的标识符类型。
C-c C-.: C-c C-, 的变体，它也会尝试推导当前洞的内容的类型。
C-c C-SPC: 给出。检查当前洞中项的类型是否正确，若正确，则用该项替换此洞。
C-c C-r: 精化。检查洞中表达式 e 的类型是否与期望的类型匹配。若匹配，则该洞会被替换为 e { }1 ... { }n，这里会插入足够数量的新洞。若洞为空，那么精化命令则会插入一个 lambda 或构造子（如果有唯一类型正确的选择）。
C-c C-c: 分类讨论。若光标在一个表示定义右式的洞里，那么此命令会自动对你选择的变量执行模式匹配。
C-c C-n: 规范化。系统会请求一个接下来要求值的项。
M-.: 跳转到定义。跳转到光标下标识符的定义处（如果已知的话）。
M-*: 返回（Emacs < 25.1）
M-,: 返回（Emacs ≥ 25.1）

更多关于 Emacs 模式的信息（配置、键位绑定、Unicode 输入等）见 Emacs Mode。

菜单¶

系统中有两个主要的菜单：

主菜单叫做 Agda2，用于全局命令
上下文相关的菜单会在你在洞中点击右键时出现。

菜单包含了比前面所列更多的命令。见全局和上下文相关命令。

在源码中输入数学符号¶

Agda 在源码文件中使用 Unicode 字符（确切来说是 UTF-8 字符编码）。几乎任何字符都可以用作标识符（如 ∀、α、∧ 或 ♠ 等），因此大部分词法单元之间都需要空格。

很多数学符号都可以使用对应的 LaTeX 命令输入。例如，你可以按下 \forall 来输入 ∀。关于如何输入多种字符的详细描述可参见此处。

（注意，若你使用其他程序阅读 Agda 代码，请确保它在解码源文件时使用了正确的字符集编码。）

错误¶

若某个文件无法通过类型检查，Agda 会给出解释。通常光标会跳转到错误的位置，默认情况下该错误会由下划线标出。然而有些错误的标记方式稍微有些不同。如果 Agda 无法确定某个定义是否停机/可归约，那么它会以浅肉色高亮，若除了目标之外的元变量无法得出，那么该处代码会以黄色高亮（在你重新加载该文件之前，高亮可能不会显示）。在出现后面这种错误时，你仍然可以在该文件中工作，但 Agda 默认会拒绝将它导入其它模块中，若你的函数不会停机，那么 Agda 可能会卡住。

如果你不喜欢错误高亮的方式（例如色盲），那么可以在 Emacs 中加载了 Agda 文件后，输入 M-x customize-group RET agda2-highlight RET 并遵从指示来调整设置。

编译 Agda 程序¶

要编译针对某个 A 的函数 main :: IO A （其中的 IO 可在 Primitive.agda 中找到）所在的模块，请使用 C-c C-x C-c。若该模块名为 A.B.C，那么编译出的二进制文件会命名为 C （位于项目顶级目录的 A 目录下）。

批处理模式命令¶

还有一个批处理模式的命令行工具 agda。要查看更多关于此命令的信息，请使用 agda --help。