Agda User Manual v2.6.1.1

• 语言: 英语
• 格式: .epub
• 来源: agda.readthedocs.io

摘要

文档主要介绍了Agda编程语言的用户手册，涵盖了Agda的基本信息、命令行选项、错误处理、警告标志以及模式匹配的相关内容。文档详细说明了Agda的安装、使用、编译等操作，并提供了相关的命令和选项，如--help、--interaction、--version等。此外，文档还讨论了Agda的错误处理机制，包括如何处理未解决的元变量和非终止代码，并介绍了模式匹配的相关设置。文档还提供了如何使用Agda进行编译和调试的指导，以及如何在其他编辑器中使用Agda。

AI总结

《Agda 用户手册 v2.6.1.1》 是 Agda 编程语言的官方文档，提供了语言特性、工具使用和相关资源的详细说明。以下是文档的核心内容总结：

### 1. **命令行选项**
Agda 提供了多个命令行选项来控制其行为：
- `--injective-type-constructors`：启用注入型类型构造器，使 Agda 变为反直觉类型系统（anti-classical），可能带来不一致性。
- `--rewriting`：启用重写规则的声明和使用。
- `--allow-incomplete-matches`：忽略模式匹配不完整的情况，成功生成接口文件。
- `--allow-unsolved-metas`：忽略未解决的元变量，成功生成接口文件。
- `--no-positivity-check` 和 `--no-termination-check`：禁用严格正交性和终止性检查。
- `--warning={GROUP|FLAG}` 和 `-W {GROUP|FLAG}`：设置警告组或标志。

### 2. **模式匹配与等式**
- `--exact-split` 和 `--no-exact-split`：控制定义中的所有子句是否需要作为定义等式。
- `--no-eta-equality`：默认情况下，记录不具有Eta等价性。
- `--no-flat-split`：禁用对 `@` 引论的模式匹配。

### 3. **错误与警告**
- Agda 会突出显示非终止或未解决的元变量（黄色高亮），但不会阻止编辑。
- 提供颜色定制选项，以适应不同用户的需求。

### 4. **工具与资源**
- **交互模式**：支持 Emacs 模式和 JSON 模式（Atom 等编辑器）。
- **编译工具**：使用 `agda` 命令行工具进行批处理编译。
- **调试与测试**：通过 `make user-manual-test` 检查文档中的代码示例是否正确。

### 5. **语言特性**
- **依赖类型与模块系统**：支持依赖类型、模块化和并置模式（copatterns）。
- **代码示例**：文档中的代码示例分为“可见且已验证”和“不可见”两种类型，确保用户代码的正确性。

### 6. **贡献与文档**
- Agda 及其相关库托管在 GitHub，欢迎贡献代码和文档。
- 用户可以通过拉取请求或问题报告参与文档的完善。

### 7. **学习与资源**
- 对于新手，推荐从 Agda Wiki 和《Getting Started》章节入手。
- 提供丰富的教程、指南和参考资料。

### 8. **安装与使用**
- 安装 Agda 可通过 Hackage 或从开发版本编译。
- 编译程序时，使用 `C-C C-x C-c` 或 `agda` 命令行工具。

### 总结
《Agda 用户手册》 是一个仍在完善中的文档，内容涵盖 Agda 的核心语言特性、工具使用和资源获取方式。对于新手和开发者，文档提供了丰富的学习资料和实践指南，同时支持用户通过 GitHub 贡献和反馈问题。