Agda User Manual v2.5.4

《Agda User Manual v2.5.4》是Agda编程语言及其相关工具的官方文档，内容涵盖Agda的语言特性、工具使用、库管理、贡献指南等。以下是文档的核心内容总结： --- ### 1. **概述** - Agda是一门依赖类型的编程语言，支持类型检查、编译和编辑。 - 本手册分为多个部分，包括语言参考、工具使用、库管理和贡献指南等。 - 手册仍在完善中，欢迎通过GitHubissue或pull request贡献。 --- ### 2. **语言参考** - **核心特性**： - 支持抽象定义、内置类型、共同归纳、核心语言、外部函数接口等。 - 提供函数定义、函数类型、隐式参数、实例参数、无关性、λ抽象、局部定义（`let` 和 `where`）等功能。 - 支持模式同义词、正性检查、假设、pragma、记录类型、反射、重写、安全Agda、大小类型、语法糖、望远镜、终止检查、宇宙级别、`with`抽象等。 - **语法与结构**： - 提供字面重载、混合固定运算符、模块系统、相互递归等。 - 支持Unicode输入和语法高亮。 --- ### 3. **工具使用** - **自动证明搜索（Auto）**： - 支持通过`Auto`命令搜索类型的实例并填充空白。 - 可用于交互式构造证明或程序。 - 底层基于Agsy算法，支持超时机制和选项（如`-t`设置超时、`-c`允许分情况分析）。 - **命令行选项**： - 包括版本信息、帮助信息、交互模式、编译选项（如`--no-main`、`--compile-dir`）、生成高亮代码（如`--vim`、`--latex`）等。 - **Emacs模式**： - 提供快速入门指南、键绑定、Unicode输入支持、高亮显示。 - 支持文档生成（如Literate TeX、reStructuredText、Markdown）。 - **类型检查与文档生成**： - 文档以reStructuredText格式编写，支持本地渲染。 - 代码示例可嵌入文档，扩展名为`.lagda.rst`时会被Agda检查。 --- ### 4. **库管理** - **标准库**： - 标准库使用了许多不安全特性（如`postulate`），这些特性尚未隔离。 - 因此，依赖标准库的项目无法在`--safe`模式下通过类型检查。 - 目前正在修复此问题。 - **库安装与使用**： - 支持通过`agda-stdlib`管理库。 - 提供默认库、版本号、升级指南等。 --- ### 5. **安全Agda** - 使用`--safe`选项可以禁用可能导致不一致的特性。 - 不兼容的特性包括： - `postulate`（假设公理）。 - `--allow-unsolved-metas`（允许未解决的元变量）。 - `--no-positivity-check`（不检查正性）。 - `--no-termination-check`（不检查终止）。 - `--type-in-type`（允许类型在类型中）。 - `--injective-type-constructors`（注入性类型构造器）。 - `--experimental-irrelevance`（实验性无关性）。 - `--rewriting`（重写）。 --- ### 6. **已知问题** - **Pragma选项**： - 文件顶部的`{-# OPTIONS --safe #-}`可能不生效（#2487）。 - **库兼容性**： - 标准库的不安全特性导致`--safe`模式下无法正常使用。 --- ### 7. **贡献与文档** - 文档本地渲染需要Python、Sphinx和dvipng。 - 代码示例支持嵌入文档，并可通过`make user-manual-test`检查类型正确性。 - 提交文档前需使用`fix-agda-whitespace`去除尾部空格。 --- 本手册详细介绍了Agda的核心功能、工具使用和库管理，同时强调了安全特性和贡献指南，是Agda语言的重要参考资料。