Agda User Manual v2.6.1.1

《Agda User Manual v2.6.1.1》中文总结 本文是对Agda编程语言及其相关工具的用户手册v2.6.1.1的总结，涵盖了核心功能、配置选项、编辑工具和文档贡献指南等内容。 ### 1. **命令行选项** - **常用选项**： - `--help`：显示帮助信息。 - `--interaction` 和 `--interaction-json`：用于Emacs和其他编辑器的交互模式。 - `--version`：显示版本号。 - **类型检查与编译选项**： - `--caching`：启用/禁用类型检查缓存，默认启用。 - `--allow-incomplete-matches`：允许不完整的模式匹配定义。 - `--allow-unsolved-metas`：允许未解决的元变量。 - `--no-positivity-check` 和 `--no-termination-check`：分别禁用严格正性数据类型和终止检查的警告。 ### 2. **模式匹配与等式** - `--exact-split`：要求定义中的所有子句作为定义等式，除非标记为CATCHALL。 - `--no-eta-equality`：默认.records为无-eta-equality。 ### 3. **实验性特性** - `--experimental-irrelevance`：启用不相关级别和数据匹配的不相关特性。 - `--injective-type-constructors`：启用注入型构造函数。 - `--confluence-check`：启用REWRITE规则的可合流性检查。 - `--cubical`：启用立方体特性。 ### 4. **增量重建模式** - `--no-projection-like`：关闭投影样分析。 - `--only-scope-checking`：仅执行顶级模块的作用域检查，不执行类型检查。 ### 5. **文档贡献指南** - Agda及其相关库托管在GitHub，欢迎通过 Fork仓库、提交变更并创建Pull Request进行贡献。 - 文档以.rest格式编写，嵌入的Agda代码会被类型检查。 - 提交前请清理末尾空白字符。 ### 6. **其他选项** - 打印与调试选项： - `--no-unicode`：禁用unicode字符打印。 - `--show-implicit` 和 `--show-irrelevant`：分别显示隐式和不相关参数。 - `--verbose`：设置详细程度。 - 其他功能： - `--copatterns`：启用/禁用共模式匹配定义，默认启用。 - `--postfix-projections`：使后缀投影表示成为默认。 ### 总结 本手册详细介绍了Agda编程语言的核心功能、配置选项和使用指南，同时鼓励用户通过GitHub参与开发和文档完善。用户可以根据自身需求调整命令行选项，以优化类型检查和编译过程。