Agda User Manual v2.6.2.1

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

摘要

该文档是Agda编程语言2.6.2.1版本的用户手册，由Agda团队编写，发布于2021年12月8日。手册概述了Agda作为依赖类型编程语言和证明助手的功能，包括安装、交互式开发、编译和编辑系统。文档详细介绍了语言参考，如抽象定义、内置模块、余归纳、协模式、核心语言、覆盖检查、立方体类型、累积性、数据类型、外部函数接口、函数定义、隐式参数、实例参数、无关性、模式同义词、积极性检查等。此外，还涵盖了命令行选项和编译指令，如缓存、打印调试、协模式与投影、实验性功能（如汇合检查、立方体、重写规则）、错误与警告（如允许不完整匹配、未解决元变量）、模式匹配与等式（如精确分割、无eta等式、无模式匹配）。文档还提供了贡献指南，说明如何通过GitHub参与开发，并指出用户手册仍在完善中，欢迎贡献。

AI总结

《Agda用户手册v2.6.2.1》主要内容总结如下：

**一、概述**
该手册是Agda编程语言及其类型检查、编译、编辑系统和相关资源的官方文档。手册仍在完善中，欢迎贡献。

**二、入门指南**
- **Agda简介**：一种依赖类型编程语言和证明助手。
- **安装**：可使用cabal安装，支持多版本共存（通过`--program-suffix`切换）。
- **Hello World示例**：
- **交互式**：定义`Greeting`数据类型和`greet`函数，在Emacs中加载验证。
- **可执行程序**：通过`postulate`声明`putStrLn`，使用GHC后端编译为二进制文件。
- **交互式开发**：支持Emacs、Atom、VSCode、Vim等编辑器，提供类型检查、归一化、案例分割等命令。

**三、语言参考（核心特性）**
涵盖抽象定义、内置模块、余归纳、协模式、核心语言、覆盖检查、立方类型、累积性、数据类型、扁平模态、外部函数接口、函数定义与类型、变量泛化、守卫立方、隐式参数、实例参数、无关性、Lambda抽象、局部定义、词法结构、字面量重载、混合运算符、模块系统、相互递归、模式同义词、正性检查、假设、重写、反射、记录类型、大小类型、终止检查、无K公理、警告等。

**四、工具与选项**
- **命令行选项**：包括缓存控制（`--caching`）、打印控制（`--no-unicode`、`--show-implicit`）、库路径（`--include-path`）、库选择（`--library`）等。
- **实验性功能**：`--cubical`（启用立方类型）、`--rewriting`（启用重写规则）、`--injective-type-constructors`（单射类型构造器，可能导致不一致）等。
- **错误与警告**：`--allow-incomplete-matches`（允许不完整匹配）、`--allow-unsolved-metas`（允许未解元变量）、`--no-positivity-check`（禁用正性检查）、`--no-termination-check`（禁用终止检查）等。
- **模式匹配与等式**：`--exact-split`（要求定义性等式）、`--without-K`（禁用K公理）、`--keep-pattern-variables`（保留模式变量）等。
- **搜索深度**：`--instance-search-depth`（实例搜索深度，默认500）、`--inversion-max-depth`（模式匹配反转最大深度，默认50）、`--termination-depth`（终止检查深度，默认1）。
- **其他**：`--double-check`（双重类型检查）、`--guardedness`（守卫余递归）、`--irrelevant-projections`（无关投影，可能导致不一致）、`--auto-inline`（自动内联）、`--call-by-name`（按名调用）等。

**五、贡献与文档**
- **贡献方式**：通过GitHub提交Pull Request或Issue，标签包括`difficulty: easy`和`help wanted`。
- **文档格式**：使用reStructuredText，位于`doc/user-manual`目录，自动发布至`https://agda.readthedocs.io`。
- **本地构建**：需安装Python ≥ 3.3、Sphinx、sphinx-rtd-theme和ImageMagick。