Agda User Manual v2.6.2.2

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

摘要

本文档是Agda 2.6.2.2版本的用户手册，由Agda团队于2022年6月3日发布。手册概述了Agda作为编程语言和证明助手的功能，包括类型检查、编译和编辑系统。文档包含多个章节：概述、入门指南、语言参考和工具。入门部分介绍了Agda的安装、'Hello world'程序示例以及交互式开发环境。语言参考详细描述了抽象定义、内置类型、余归纳、协模式、核心语言、覆盖检查、立方类型、累积性、数据类型、外部函数接口、函数定义、隐式参数、实例参数、不可关联性、Lambda抽象、局部定义、词法结构、字面量重载、模式同义词、重写规则和运行时不可关联性等特性。工具部分涵盖了命令行选项，如编译选项、警告控制、模式匹配和等式设置。文档还提到手册仍在完善中，欢迎贡献。

AI总结

该文档是《Agda用户手册 v2.6.2.2》的目录和内容摘要，主要涵盖以下核心内容：

1. **Agda简介与入门**：Agda是一种依赖类型编程语言，可用于编写程序、证明定理和编译为可执行文件。文档提供了安装指南、一个完整的“Hello World”示例以及交互式开发环境的介绍（支持Emacs、Atom、VSCode等编辑器）。

2. **语言参考**：详细描述了Agda的语言特性，包括抽象定义、内置类型、共归纳、协模式、数据类型、函数定义、隐式参数、实例参数、模块系统、模式同义词、重写规则等。

3. **编译与工具**：介绍了Agda的编译系统，支持GHC和JavaScript后端。提供了多种命令行选项，例如启用/禁用特定特性（如Cubical、无K公理）、设置搜索深度、生成高亮代码（HTML/LaTeX）、以及管理库和依赖。

4. **高级特性**：
- **重写规则**：允许用户定义自定义的等式重写规则，并可选择性地进行汇合性检查。
- **运行时不可达性**：支持使用`@0`或`@erased`注解标记在运行时被擦除的值，从而优化编译输出。
- **实验性功能**：包括单射类型构造器、不安全性、以及基于守卫的共递归等。

5. **贡献与资源**：手册仍在完善中，欢迎通过GitHub提交Pull Request或Issue。文档使用reStructuredText格式编写，并托管在Read the Docs上。