Agda User Manual v2.5.3

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

摘要

该文档是Agda 2.5.3版本的用户手册，主要介绍了Agda的安装、语言特性、工具使用及与Haskell的交互。安装部分涵盖了Debian/Ubuntu、Fedora和NixOS等系统的安装方法。语言参考部分详细描述了抽象定义、内置类型、共归纳、协模式、数据类型、外部函数接口、函数定义、隐式参数、实例参数、无关性、Lambda抽象、局部定义、词法结构、字面量重载、混合操作符、模块系统、互递归、模式同义词、正性检查、假设、编译指示、记录类型、反射、重写、安全Agda、有界类型、望远镜、终止检查和宇宙层次等内容。工具部分重点介绍了自动证明搜索工具Auto，可搜索类型居民并填充孔洞。此外，文档还说明了如何使用COMPILE pragma将Agda类型映射到Haskell类型，包括不透明类型和数据类型的映射，以及内置类型与Haskell类型的对应关系。文档最后包含了许可证信息。

AI总结

Agda 用户手册 v2.5.3 核心内容总结：

**1. 文档概况**
- 版本：2.5.3，发布于2017年9月8日
- 主要开发者包括 Ulf Norell、Andreas Abel 等，并列出多位贡献者
- 采用 MIT 许可证开源

**2. 核心语言特性（31项）**
涵盖抽象定义、内置类型、余归纳、协模式、核心语言、数据类型、外部函数接口、函数定义与类型、隐式/实例参数、无关性、Lambda抽象、局部定义、词法结构、字面量重载、混合操作符、模块系统、互递归、模式同义词、正性检查、公设、编译指示、记录类型、反射、重写、安全模式、有界类型、望远镜、终止检查、宇宙层级等

**3. 工具与开发支持**
- **自动证明搜索（Auto）**：基于Agsy算法，支持超时设置、大小写拆分、提示使用等选项，可辅助交互式构造项
- **文档编写**：使用 reStructuredText 格式，支持 `.lagda.rst` 扩展名实现代码示例的类型检查
- **本地构建**：需 Python 3.3+、Sphinx、LaTeX 和 dvipng

**4. 外部函数接口（FFI）**
- 支持与 Haskell 互操作，通过 `COMPILE GHC` 编译指示实现类型映射
- 提供四种编译指示形式：函数代码映射、类型映射、数据类型映射、名称暴露
- 内置类型映射表：Nat→Integer、String→Data.Text.Text、Bool→Boolean 等

**5. 安装方式**
- Debian/Ubuntu：`apt-get install agda-mode`
- Fedora：`yum install Agda`
- NixOS：`nix-env -iA haskellPackages.Agda`

**6. 代码示例规范**
- 可见且需类型检查的代码使用 `::` 前缀
- 支持模块作用域限定
- 可通过 `make user-manual-test` 验证所有示例类型正确性