Agda User Manual v2.6.1

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

摘要

文档是关于Agda编程语言及其相关工具的用户手册，涵盖了安装、语法、命令行选项等内容。手册详细介绍了Agda的类型检查和编译系统，并提供了代码示例的编写和验证方法。此外，还介绍了如何为Agda手册做贡献，包括如何提交修复和改进。手册还涉及了Agda的高级功能，如copatterns、projections等，并提供了相关的命令行选项和配置方法。

AI总结

以下是对《Agda User Manual v2.6.1》文档内容的简要总结，重点突出核心观点和关键信息，逻辑连贯，语言简洁明了：

---

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

#### 1. **手册概述**
- 本手册是Agda编程语言及其相关工具的官方文档，目前仍在完善中，欢迎贡献。
- 可从GitHub Actions下载最新PDF版本，或访问Agda Wiki获取更多资源（如教程、文档等）。

#### 2. **Agda简介**
- Agda是一种基于类型的编程语言，支持类型检查、编译和编辑系统。
- 适合新手的资源包括Agda Wiki和“Getting Started”章节。
- 语言参考章节详细描述了Agda语言的语法和核心功能。

#### 3. **主要功能**
- **类型检查与编译**：支持类型推导、模式匹配、依赖类型等。
- **高级特性**：
- Coinduction（共归纳）、Copatterns（协模式）、Cubical（立方体类型理论）。
- Cumulativity（累加性）、Data Types（数据类型）、Flat Modality（模态）等。
- **工具与资源**：
- Foreign Function Interface（FFI，外部函数接口）。
- 模块系统、互归归、模式同义词等功能。
- 支持隐式参数、局部定义和字面过载。

#### 4. **新功能（版本2.6.1）**
- `--allow-incomplete-matches`：允许不完全匹配的模式匹配定义。
- `--allow-unsolved-metas`：允许未解元变量。
- `--no-flat-split`：禁用@♭参数上的模式匹配。
- 新增`--interaction-json`选项，支持与其他编辑器（如Atom）交互。

#### 5. **命令行选项**
- **一般选项**：
- `--help`：显示帮助信息。
- `--interaction`：与Emacs模式配合使用。
- `--version`：显示版本号。
- **类型检查与编译**：
- `--only-scope-checking`：仅执行作用域检查。
- `--no-positivity-check`：禁用严格正定性检查。
- **模式匹配与等式**：
- `--exact-split`：要求所有定义子句作为定义等式。
- `--no-eta-equality`：默认禁用Eta等同性。
- **打印与调试**：
- `--no-unicode`：不使用Unicode字符显示。
- `--show-implicit`：显示隐式参数。
- **实验性功能**：
- `--confluence-check`：启用REWRITE规则的可合流性检查。
- `--cubical`：启用立方体特性。
- `--injective-type-constructors`：启用注入式类型构造。

#### 6. **文档与贡献**
- 使用`.lagda.rst`扩展名的文档文件会被Agda识别并类型检查。
- 文档中的代码示例需通过`make user-manual-test`验证。
- 贡献者需通过GitHub fork仓库并提交Pull Request（PR），可参考标签`difficulty: easy`和`help wanted`。

#### 7. **其他工具与资源**
- `agda-ghc-names`：将生成的Haskell代码名称映射回Agda名称。
- "Search About"功能（自版本2.5.1起）：在作用域中搜索定义，支持按标识符和子字符串匹配。

---

以上是《Agda User Manual v2.6.1》的核心内容和关键信息的总结，旨在帮助读者快速了解Agda的主要功能、使用方法和新特性。