Agda User Manual v2.6.4

### 总结 本文主要总结了《Agda User Manual v2.6.4》中的核心内容，以下是总结的要点： #### 1. 新功能 - **版本2.6.4**新增了多项功能和命令行选项，包括： - `--hidden-argument-puns` 和 `--no-hidden-argument-puns`，默认禁用。 - `--no-guarded`，默认启用，表示禁用guarded类型理论。 - `--no-injective-type-constructors`，默认启用，表示禁用注入型构造器。 - `--no-lossy-unification`，默认启用，表示禁用无损统一。 - `--no-pattern-matching`，默认禁用，表示启用模式匹配。 - `--no-prop`，默认禁用，表示禁用Prop的声明和使用。 - `--no-rewriting`，默认启用，表示禁用重写规则。 - `--no-two-level`，默认启用，表示禁用两级类型理论。 - `--allow-incomplete-matches` 和 `--no-allow-incomplete-matches`，默认禁用。 - `--allow-unsolved-metas` 和 `--no-allow-unsolved-metas`，默认禁用。 - `--positivity-check` 和 `--no-positivity-check`，默认启用。 - `--termination-check` 和 `--no-termination-check`，默认启用。 #### 2. 错误和警告 - **错误处理**： - `--allow-incomplete-matches` 和 `--no-allow-incomplete-matches`，控制是否允许不完整的匹配定义。 - `--allow-unsolved-metas` 和 `--no-allow-unsolved-metas`，控制是否允许未解的元变量。 - **警告设置**： - `--warning={GROUP|FLAG}` 和 `-W {GROUP|FLAG}`，用于设置警告组或标志。 #### 3. 模式匹配和相等性 - **模式匹配**： - `--exact-split` 和 `--no-exact-split`，控制是否要求所有子句作为定义相等。 - **相等性**： - `--eta-equality` 和 `--no-eta-equality`，控制是否启用eta相等性。 - `--cohesion` 和 `--no-cohesion`，控制是否启用cohesion modalities。 - `--flat-split` 和 `--no-flat-split`，控制是否启用@♭参数的模式匹配。 #### 4. 编译和生成 - **编译选项**： - `--compile-dir={DIR}`，设置编译输出目录。 - `--no-main` 和 `--main`，控制是否将当前模块视为主模块。 - `--with-compiler={PATH}`，设置编译器路径。 - **高亮源码生成**： - `--count-clusters` 和 `--no-count-clusters`，控制是否计数扩展grapheme clusters。 - `--css={URL}`，设置CSS文件的URL。 #### 5. 安装指南 - **安装依赖**： -่อนติดตั้งAgda，需要安装Python、Sphinx、LaTeX、PyDvi等工具。 - **构建文档**： -使用`make html`或其他目标命令生成文档。 - **安装标志**： -支持多个安装标志，包括`debug`、`enable-cluster-counting`、`optimise-heavily`等。 #### 6. 文档贡献 -文档使用reStructuredText格式，贡献者可以通过GitHub Fork并提交Pull Request。 -文档构建需要安装Sphinx和相关工具，可以本地构建并发布到https://agda.readthedocs.io。 以上是《Agda User Manual v2.6.4》的核心内容总结，涵盖了新功能、命令行选项、错误与警告、模式匹配、编译选项、安装指南和文档贡献等部分。