Agda User Manual v2.5.4.1

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

摘要

The Agda User Manual v2.5.4.1 provides comprehensive guidance on the Agda programming language, its type checking, compilation, and editing system. It covers interactive editing in Emacs or Atom, type checking using placeholders called 'holes', and tools like Auto for automated proof search. The manual also details documentation practices, including embedding code examples and ensuring type correctness. Additionally, it explains library management and integration with the standard library.

AI总结

《Agda 用户手册》是 Agda 编程语言的官方文档，介绍了 Agda 的语言特性、工具和使用方法。以下是文档的核心内容总结：

### 1. 概述
Agda 是一个基于依赖类型理论的编程语言，支持交互式开发、类型检查和编译。文档提供了语言参考、工具使用和开发指南。

### 2. 快速入门
#### 2.1 先决条件
- 需要安装 Haskell（GHC）、Python 3.3 以上版本、LaTeX 和 dvipng。
- 支持的开发环境包括 Emacs 和 Atom。

#### 2.2 安装
- **稳定版本**：通过包管理器安装（如 Homebrew、Nix 包管理器）。
- **开发版本**：从源码安装，需先获取代码并运行 `make install`。
- 安装时可选参数包括 `--without-stdlib` 和 `--without-ghc`。

#### 2.3 快速上手
- **编辑**：使用 Emacs 或 Atom 打开 `.agda` 文件。
- **类型检查**：使用 `C-c C-1` 检查文件，`C-c C-` 查看当前目标类型。
- **填充空洞**：使用 `C-c C-SPC` 填充空洞，`C-c C-r` 进行 refine 操作。

### 3. 语言特性
- **核心语言**：支持依赖类型、联合递归、模式匹配和反射。
- **数据类型**：包括枚举类型、记录类型和大小受限类型。
- **工具与特性**：
- **自动证明搜索（Auto）**：通过 Agsy 算法自动寻找类型 inhabitant。
- **反射**：允许在运行时操作类型和证明。
- **安全 Agda**：提供类型安全保证。
- **宇宙层级**：支持高级的依赖类型理论。

### 4. 工具
- **库管理**：
- 创建 `libraries` 文件指定库路径。
- 创建 `defaults` 文件设置默认库。
- **文档生成**：
- 使用 `make html` 生成 HTML 文档。
- 使用 `make latex` 生成 LaTeX 文档。
- **类型检查代码示例**：在 `.lagda.rst` 文件中嵌入 Agda 代码并进行类型检查。

### 5. 贡献
- 文档使用 reStructuredText 格式编写，可通过 `make user-manual-test` 检查所有示例的正确性。
- 提交文档前需运行 `fix-agda-whitespace` �移除尾随空白。

### 6. 特殊说明
- Agda 支持多种语言特性（如反射、联合递归、模式同义词等），并提供丰富的工具支持（如自动证明搜索、库管理、文档生成等）。
- 文档强调了交互式开发的重要性，并提供了详细的命令和操作指南。

### 总结
《Agda 用户手册》全面介绍了 Agda 的语言特性和工具使用方法，适合编程语言研究者和依赖类型理论的开发者阅读。文档结构清晰，提供了从安装到高级功能的详细指导。