Agda User Manual v2.6.2

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

摘要

文档是Agda编程语言的用户手册，介绍了其类型检查、编译和编辑系统及相关工具。手册仍在完善中，欢迎贡献。手册包括Getting Started、Language Reference和Tools等部分，详细描述了Agda的功能和使用方法，如命令行选项、类型检查选项、Cubical功能、Projection-likeness优化和Copatterns定义等。

AI总结

《Agda User Manual v2.6.2》是Agda编程语言及其相关工具的用户手册，目前仍在完善中，欢迎贡献和修正。以下是手册的主要内容和关键信息总结：

### 1. 手册概述
- **目的**：手册介绍了Agda编程语言、类型检查、编译及编辑系统等功能。
- **获取**：最新PDF版本可从GitHub Actions获取，相关资源可在Agda Wiki上找到。
- **推荐**：新手应优先参考Agda Wiki和“Getting Started”章节，而非直接阅读“Language Reference”。

### 2. 贡献指南
- **方式**：通过GitHub仓库提交Pull Request或Issue。
- **注意事项**：需阅读HACKING.md文件，了解代码规范和行为准则。
- **任务标签**：可通过标签“difficulty: easy”和“help wanted”找到入手任务。

### 3. 功能概述
- **语言参考**：详细描述了Agda语言的核心特性，包括抽象定义、内建类型、共归纳、懒_evaluation等。
- **工具使用**：介绍了Agda编辑和编译系统的用法。
- **重要功能**：支持代码示例的类型检查和渲染，确保文档中的代码正确性。

### 4. 命令行选项
- **一般选项**：包括显示帮助（`--help`）、版本号（`--version`）等。
- **交互模式**：支持Emacs和其他编辑器的交互式使用。
- **优化与调试**：如关闭投影分析（`--no-projection-like`）和仅作用域检查（`--only-scope-checking`）。
- **缓存与编译**：控制类型检查缓存和编译选项。
- **打印与调试**：包括隐式参数显示（`--show-implicit`）、不使用Unicode字符（`--no-unicode`）等。
- **模式匹配与相等性**：支持模式匹配和等式定义。

### 5. 实验性功能
- **_cube特性_：启用立方体类型理论。
- **重写规则**：支持REWRITE规则的声明与使用，配备汇聚性检查。

### 6. 错误与警告
- **容错选项**：允许不完全匹配和未解决的元变量。
- **警告设置**：可自定义警告组或标志。

### 7. 文档与代码示例
- **渲染方式**：支持局部渲染文档，确保代码示例的正确性。
- **代码语法**：代码示例分为可见和不可见两类，均会被Agda类型检查。

### 8. 搜索定义
- **使用方法**：通过goal菜单或快捷键invoke搜索功能。
- **搜索逻辑**：基于定义中的标识符和字符串子串匹配相关内容，支持模糊查找，如搜索涉及特定字符串或模块的定义。

### 总结
本手册详细介绍了Agda语言及其工具的使用方法，强调了社区贡献的重要性，并提供了丰富的资源和实用工具，帮助用户高效地使用和理解Agda系统。