Agda User Manual v2.6.1.2

以下是对《Agda User Manual v2.6.1.2》内容的总结，按照文档结构和内容层次进行梳理，重点突出核心观点和关键信息： --- ### **Agda 用户手册 v2.6.1.2 总结** #### **1. 概述** - Agda 是一个基于依赖类型理论的编程语言，支持类型检查、编译和编辑系统等功能。 - 本手册是未完成的工作，欢迎通过 GitHub 提交Pull Request或修复问题来贡献内容。 - 最新版本手册可从 GitHub Actions 下载，相关资源（如教程、文档）可在 Agda Wiki 上找到。 #### **2. 命令行选项** - **一般选项**： - `--help`: 显示帮助信息。 - `--interaction` 和 `--interaction-json`: 用于与编辑器（如 Emacs 或 Atom）交互。 - `--version`: 显示版本号。 - `--only-scope-checking`: 只进行作用域检查，不进行类型检查。 - **警告和错误**： - `--allow-incomplete-matches`: 允许不完整的模式匹配定义。 - `--allow-unsolved-metas`: 忽略未解元变量。 - `--no-positivity-check` 和 `--no-termination-check`: 禁用正性检查和终止检查。 - `--warning`: 设置警告组或标志。 - **缓存**： - `--caching`: 启用类型检查缓存（默认）。 - **打印和调试**： - `--no-unicode`: 不使用 Unicode 字符打印项。 - `--show-implicit` 和 `--show-irrelevant`: 显示隐式和不相关的参数。 - `--verbose`: 设置冗余级别。 - **模式匹配与相等性**： - `--exact-split` 和 `--no-exact-split`: 是否要求所有定义子句为定义等式。 - `--no-eta-equality`: 默认禁用 eta 展开。 - `--no-flat-split`: 禁止对 `@♭` 参数进行模式匹配。 - **其他功能**： - `--copatterns`: 启用协模式匹配（默认）。 - `--postfix-projections`: 使用后缀投影表示法（默认）。 - `--confluence-check`: 启用重写规则的汇聚性检查（新功能）。 - `--cubical`: 启用立方体类型理论功能。 - `--injective-type-constructors`: 启用注入型类型构造（可能导致不一致）。 #### **3. 开发与社区参与** - Agda 源代码和相关库托管在 GitHub，欢迎 Fork 并提交 Pull Request。 - 贡献前请查阅 `HACKING.md` 文件，解决标记为“难度：易”或“需要帮助”的问题。 - 手册和代码示例可以通过 `make user-manual-test` 进行类型检查。 #### **4. 文档渲染与代码示例** - 本地渲染文档：文档文件以 `.lagda.rst` 扩展名保存，Agda 会自动识别并类型检查代码。 - 代码示例语法： - 可见且经过类型检查的代码示例应使用 `::` 语法，例如： ```agda data Bool : Set where true false : Bool ``` - 使用 `rst-mode` 和 `agda2-mode` 切换编辑模式。 - 提交文档前，请运行 `fix-agda-whitespace` 移除尾随空格。 #### **5. 搜索定义** - 自版本 2.5.1 起，Agda 支持通过 `Search About` Searching 对象定义的功能。 - 使用方法：在目标菜单中选择 `Search About` 或按下 `C-c C-z`。 - 输入标识符或字符串字面量，Agda 将返回匹配的定义。例如，搜索 `Char String` 会返回与字符和字符串相关的定义。 #### **6. 功能概述** - Agda 的核心语言及其扩展功能（如共归类型、立方体类型理论）在 `Language Reference` 中详细说明。 - 使用 Agda 的工具和系统的指导可在 `Tools` 章节找到。 --- 以上是手册的核心内容总结，涵盖了命令行选项、开发指南、文档使用、搜索功能等主要内容，逻辑清晰，重点突出。