Agda User Manual v2.6.4.3

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

摘要

The document provides a comprehensive manual for Agda programming language version 2.6.4.3, detailing its command-line options, debugging features, pattern matching, and library management. It covers various profiling options, experimental features, and performance optimizations, offering guidance on using Agda's editing and compilation system. The manual emphasizes the importance of user contributions for its improvement.

AI总结

以下是《Agda User Manual v2.6.4.3》文档内容的中文总结，重点突出核心观点和关键信息：

---

### 《Agda User Manual v2.6.4.3》总结

#### 1. **调试旗帜**
- `--profile={PROF}`：启用指定的分析功能，支持的选项包括 `internal`、`modules`、`definitions` 等，用于测量不同部分的性能。
- `--profile=all`：启用所有分析功能，优先选择 `internal`，可通过 `--profile=modules` 更改优先级。

#### 2. **仿射特性**
- `--copatterns` 和 `--no-copatterns`：启用或禁用共模式匹配（默认启用）。
- `--postfix-projections` 和 `--no-postfix-projections`：启用或禁用后缀投影符（默认禁用）。

#### 3. **正交性检查与终止检查**
- `--confluence-check`、`--local-confluence-check` 和 `--no-confluence-check`：启用或禁用重写规则的正交性检查（默认禁用）。
- `--termination-check`：启用终止检查（默认启用），与 `--no-termination-check` 对应。

#### 4. **警告设置**
- `--warning={GROUP|FLAG}` 和 `-W {GROUP|FLAG}`：设置警告组或旗帜。

#### 5. **模式匹配与相等性**
- `--exact-split` 和 `--no-exact-split`：要求所有定义子句作为定义等式（默认禁用）。
- `--hidden-argument-puns` 和 `--no-hidden-argument-puns`：启用或禁用隐藏参数匹配（默认禁用）。
- `--no-eta-equality` 和 `--eta-equality`：禁用或启用 eta 等式（默认禁用）。
- `--cohesion` 和 `--no-cohesion`：启用或禁用凝聚力_MODALITY（默认禁用）。
- `--flat-split` 和 `--no-flat-split`：启用或禁用 `@♭` 参数的模式匹配（默认禁用）。
- `--no-pattern-matching` 和 `--pattern-matching`：禁用或启用模式匹配（默认启用）。

#### 6. **仿色体特性与擦除仿色体**
- `--cubical` 和 `--erased-cubical`：启用仿色体特性，前者默认启用 `--cubical-compatible` 和 `--without-K`，后者是变体。

#### 7. **实验性特性**
- `--allow-exec` 和 `--no-allow-exec`：启用或禁用类型检查期间的系统调用（默认禁用）。
- `--guarded` 和 `--no-guarded`：启用或禁用锁和 tick 用于防护递归（默认禁用）。
- `--injective-type-constructors` 和 `--no-injective-type-constructors`：启用或禁用注入型构造器（默认禁用）。
- `--irrelevant-projections` 和 `--no-irrelevant-projections`：启用或禁用无关记录字段的投影（默认禁用）。
- `--lossy-unification` 和 `--no-lossy-unification`：启用或禁用一阶约束求解（默认禁用）。
- `--prop` 和 `--no-prop`：启用或禁用定义性验证无关命题（默认启用）。

#### 8. **版本与编译信息**
- `--version`、`-V` 和 `--numeric-version`：显示版本号和相关信息。
- `--print-agda-app-dir`、`--print-agda-dir` 和 `--print-agda-data-dir`：输出 Agda 应用配置或数据目录。

#### 9. **编译选项**
- `--compile-dir={DIR}`：设置编译器输出目录。
- `--main` 和 `--no-main`：启用或禁用将当前模块视为程序主模块。
- `--with-compiler={PATH}`：设置编译器路径。

#### 10. **性能优化**
- `--auto-inline` 和 `--no-auto-inline`：启用或禁用自动内联（默认禁用）。
- `--no-fast-reduce` 和 `--fast-reduce`：禁用或启用 Agda 抽象机的减少优化（默认启用）。
- `--no-forcing` 和 `--forcing`：禁用或启用强制优化（默认启用）。
- `--no-projection-like`：关闭投影分析，主要用于调试。

#### 11. **导入与库管理**
- `--ignore-interfaces`、`--ignore-all-interfaces`：忽略接口文件，强制重新类型检查。
- `--include-path={DIR}` 和 `--library={DIR}`：添加导入路径和库文件。

#### 12. **Latex 选项**
- `--latex`、`--latex-dir={DIR}` 和 `--vim`：生成带有语法高亮的 LaTeX 文件或 Vim 高亮文件。

#### 13. **其他**
- `--transliterate`：将输出中的不受支持字符替换为其他形式，仅在不使用交互式选项时生效。

---

### 注意事项
- 部分高级功能（如注入型构造器和无关投影）可能导致系统不一致，使用前需谨慎。
- 文档为持续更新中的内容，用户可通过 GitHubcontri 提供反馈或补充。

---

以上总结涵盖了 Agda 用户手册中命令行选项的核心内容，突出了各部分的功能和关键信息。