Agda User Manual v2.6.3

《Agda User Manual v2.6.3》是一份关于Agda编程语言及其工具和资源的综合指南。以下是文档的核心内容和关键信息总结： --- ### 1. **Agda核心语言** Agda是一个依赖类型的lambda calculus，其核心语言包括： - **声明**：用于引入新标识符，并指定其类型和定义。声明的内容包括数据类型、函数定义、模块、变量、模式同名词、优先级、pragma和程序选项等。 - **语法结构**：Agda的语法分为三层： - **具体语法**：用户编写的源代码（Agda.Syntax.Concrete）。 - **抽象语法**：类型检查前的中间表示（Agda.Syntax.Abstract）。 - **内部语法**：经过类型检查的核心Agda术语（Agda.Syntax.Internal）。 - **术语语法**：Agda的术语（`a`）可以是变量、lambda抽象、函数、函数空间、数据/记录类型、构造函数、种类（Seti, Set?+i）等。 --- ### 2. **Agda的内置类型** Agda提供了一些内置类型和模块，包括： - **自然数**：定义在`Agda.Builtin.Nat`中。 - **单元类型**：定义在`Agda.Builtin.Unit`中，用于某些反射类型检查操作。 - **Σ类型**：定义在`Agda.Builtin.Sigma`中，表示依赖对。 - **列表**：定义在`Agda.Builtin.List`中。 这些内置类型可以通过`BUILTIN` pragmas绑定，但建议直接使用标准库中的定义。 --- ### 3. **工具与命令行选项** Agda提供了一系列命令行选项和工具，用于编译、类型检查、代码生成和调试。常用命令行选项包括： - **模式匹配和平等性**：例如`--exact-split`、`--no-eta-equality`、`--cohesion`等。 - **编译选项**：如`--compile-dir`、`--no-main`、`--with-compiler`等。 - **生成高亮源代码**：包括LaTeX代码和依赖图的生成。 - **缓存与性能**：如`--caching`、`--no-caching`、`--profile`等。 - **警告与调试**：如`--show-implicit`、`--show-irrelevant`、`--verbose`等。 - **一致性检查**：一些选项是“感染性”的，需在依赖模块中一致使用，例如`--prop`、`--rewriting`、`--cohesion`等。 --- ### 4. **贡献指南** Agda及其相关库托管在GitHub，用户可以通过fork仓库、提交更改和创建pull request来贡献代码。文档以reStructuredText格式编写，位于`doc/user-manual`目录中，并自动发布到https://agda.readthedocs.io。贡献者可以参考`HACKING.md`文件，了解行为准则和注意事项。 --- ### 5. **其他资源** - **文档**：可以本地生成文档，依赖Python、Sphinx、ImageMagick、LaTeX等工具。 - **资源与入门**：Agda Wiki提供了丰富的教程、介绍、出版物和书籍，适合新手参考。 --- 总结来说，这份手册详细介绍了Agda的核心语言、语法、内置类型、工具使用以及贡献指南，是使用Agda进行依赖类型编程的重要参考。