Agda User Manual v2.6.4.2

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

摘要

文档主要介绍了Agda 2.6.4.2版本的用户手册，涵盖了命令行选项的使用、性能优化选项、编译与库的相关配置以及如何为Agda贡献力量。手册详细说明了各种命令行标志的功能，如--termination-check、--exact-split、--cohesion等，适用于不同的编译和类型检查场景。此外，还提供了如何编译Agda代码、设置编译器路径及库目录的指南，帮助用户更好地使用Agda进行开发和文档编写。

AI总结

《Agda User Manual v2.6.4.2》详细介绍了Agda编程语言及相关工具和资源的使用方法。以下是文档内容的总结：

---

### 1. 命令行选项
文档详细列举了Agda的命令行选项，包括：

- **终止检查**：启用或禁用终止检查默认启用，--no-termination-check禁用。
- **警告设置**：设置警告组或标志，-W {GROUP|FLAG}。
- **模式匹配与等效性**：
- --exact-split：要求定义中的所有子句都作为定义等式。
- --hidden-argument-puns：启用隐藏参数匹配，默认禁用。
- --no-eta-equality：默认禁用 eta 展开等式，--eta-equality启用。
- **凝聚模式**：启用或禁用凝聚模式，--cohesion启用，--no-cohesion禁用，默认禁用。
- **模式匹配优化**：--flat-split启用在@♭参数上的模式匹配。
- **模式匹配禁用**：--no-pattern-matching禁用模式匹配，--pattern-matching启用。

### 2. 处理与编译选项
- **编译目录设置**：--compile-dir设定编译输出目录。
- **主模块设置**：--no-main不将当前模块视为主模块，--main默认启用。
- **编译器路径**：--with-compiler设定编译器路径，GHC为默认。
- **库文件使用**：--no-default-libraries不使用默认库文件，--no-libraries禁用所有库文件，--no-interfaces禁用接口文件，--generate-interfaces生成接口文件。

### 3. 性能优化选项
- **自动内联**：--auto-inline启用自动内联，--no-auto-inline禁用，前者默认。
- **缓存类型检查**：--caching启用缓存，默认。
- **调用策略**：--call-by-name禁用询问式需要评估，--no-call-by-name默认启用。
- **强制优化**：--no-forcing禁用强制优化，--forcing启用，默认。

### 4. 其他选项
- **辅助工具**：显示版本号、Agda配置目录。
- **编码转换**：将无法显示的字符转换为其他字符。
- **umbra模式**：避免在某些环境中使用中文提示。

### 5. 文档贡献
Agda文档欢迎社区贡献，可在GitHub上fork仓库并提交Pull Request。本地渲染文档需要Python、Sphinx和LaTeX等，使用Make生成HTML文档。

---

该手册详细介绍了Agda的功能及其选项，帮助用户高效使用和贡献Agda生态系统。