Agda User Manual v2.5.4

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

摘要

《Agda User Manual v2.5.4》是Agda编程语言的用户手册，介绍了其安装、使用、编辑系统及相关工具。文档详细说明了Agda的类型检查、编译、错误处理和模块系统，并提到了自动证明搜索工具Auto的使用。手册还讨论了Agda的安全性选项和与标准库的兼容性，强调了使用--safe选项的重要性。

AI总结

《Agda User Manual v2.5.4》是Agda编程语言的官方文档，提供了对语言、工具和相关功能的详细说明。以下是文档的核心内容总结：

1. **自动证明搜索（Auto）**
Agda支持使用`Auto`命令来自动填充代码中的空洞（holes）。`Auto`基于独立于Agda的搜索算法Agsy，适用于小规模的问题，但对复杂问题的处理能力有限。
- Agsy的行为可以通过选项（如超时、使用案例分割等）进行调整。
- 已知问题：
- 案例分割模式不支持表达式分割，且有时会生成复杂的右侧代码。
- 不尊重共数据（codata）的特殊约束，将其视为普通数据（data）。
- 宇宙子类型可能导致Agsy建议的解决方案不被Agda接受。
- 宇宙多态性仅部分支持，构造宇宙多态定义时可能失败，但引用宇宙多态定义时可能成功。

2. **用户反馈**
用户可以通过GitHub问题跟踪器提交bug报告，并提供Agda无法解决但用户认为可解的例子，帮助改进Auto的性能和启发式算法。

3. **已知问题**
- 使用`--safe`选项时，标准库中大量使用不安全特性（如`postulate`），可能导致类型检查失败。
- `--safe`选项与某些特性（如`postulate`、`--allow-unsolved-metas`等）不兼容。
- 已知bug：`--safe`选项在导入文件时可能不生效。

4. **编译与错误处理**
- 编译Agda程序需定义`main :: IO A`，使用快捷键`C-C C-x C-c`或命令行工具`agda`。
- 错误处理：
- 未解决的元变量（非目标）会以黄色突出显示，但仍可编辑文件。
- 非终止函数可能导致Agda卡顿。
- 用户可通过Emacs的自定义选项调整错误高亮方式。

5. **文档管理与贡献**
- 文档采用reStructuredText格式编写，托管在GitHub仓库的`doc/user-manual`目录中。
- 用户可通过提交pull request或issue参与文档的完善。

6. **工具与语言特性**
- Agda提供丰富的语言特性，如依赖类型、共递归、反射、重写规则等。
- 提供交互式编辑模式（Agda模式）和批量命令行工具（`agda`）。

总结：Agda是一个功能强大的依赖类型编程语言，文档详细介绍了其核心功能、工具使用和开发注意事项。用户在使用过程中需注意自动工具的限制、安全模式的兼容性问题以及错误处理的最佳实践。