Agda User Manual v2.5.3

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

摘要

该文档是Agda用户手册v2.5.3，介绍了Agda编程语言及其类型检查、编译和编辑系统。文档包含语言参考章节，详细说明了抽象定义、内置类型、余归纳、协模式、数据类型、函数定义、隐式参数、实例参数、无关性、Lambda抽象、局部定义、词法结构、字面量重载、混合固定运算符、模块系统、互递归、模式同义词、正性检查、公设、编译指令、记录类型、反射、重写、安全Agda、大小类型、望远镜、终止检查、宇宙层级、With-Abstraction和Without K等特性。工具章节介绍了自动证明搜索(Auto)的使用方法和选项，以及命令行选项。文档还说明了如何编写文档、渲染本地文档和类型检查代码示例。安全Agda部分列出了与--safe选项不兼容的特性，包括公设、未解决元变量、非正性检查、非终止检查、类型中的类型、单射类型构造子等。

AI总结

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

**文档概述**
- 手册仍在完善中，欢迎通过GitHub提交贡献。
- 涵盖Agda编程语言、类型检查、编译、编辑系统及相关工具。
- 语言参考章节详细描述Agda语法；工具章节介绍编辑与编译系统。

**核心功能：自动证明搜索（Auto）**
- 自2.2.6版本支持，通过`c-c a`调用，搜索类型居民并填充目标。
- 基于Agsy算法，适用于小型问题，结果由Agda验证，含超时机制。
- 可选参数：`-t N`（超时秒数）、`-c`（允许case-split）、`-d`（尝试反驳目标）、`-l`（列出最多10个解）等。

**文档编写规范**
- 使用reStructuredText格式，代码示例需同时可见且可类型检查（`.lagda.rst`扩展名）。
- 在Emacs中可通过`M-x agda2-mode`切换Agda模式，`M-x rst-mode`切换回rST模式。
- 运行`make user-manual-test`可验证所有代码示例的类型正确性。

**安全模式（Safe Agda）**
- 通过`--safe`选项禁用可能导致不一致的特性，包括：
- `postulate`（假设任意公理）
- `--allow-unsolved-metas`（接受未完成证明）
- `--no-positivity-check`（允许非严格正的数据类型）
- `--no-termination-check`（允许循环程序）
- `--type-in-type`（允许Girard-Hurken悖论）等。
- **已知问题**：文件内`{-# OPTIONS --safe #-}`对导入文件无效，仅命令行选项可靠。
- **标准库**：大量使用不安全特性（如FFI中的`postulate`），导致`--safe`下无法通过类型检查，修复工作正在进行中。

**命令行选项**
- 通用选项：`--version`（显示版本）、`--help`（显示帮助）、`--interactive`（交互模式，已不再支持）。
- 编译选项：`--no-main`（不将模块视为主程序）、`--compile-dir=DIR`（设置编译输出目录）、`--no-forcing`（禁用强制优化）。
- 高亮源码生成：`--vim`（Vim高亮）、`--latex`（LaTeX高亮）、`--html`（HTML高亮）。

**其他工具与功能**
- **重写（Rewriting）**：手册仅作简要提及，未展开说明。
- **库管理**：包括库文件安装、使用、默认库、版本号及升级指南。
- **已知问题**：安全模式下的选项传播缺陷（#2487）。

**文档贡献须知**
- 提交前需运行`fix-agda-whitespace`移除尾部空白。
- 持续集成会自动检查文档中的代码示例。