Agda User Manual v2.5.4.1

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

摘要

本文档是Agda用户手册v2.5.4.1，介绍了Agda编程语言及其类型检查、编译和编辑系统。文档包含语言参考、工具使用指南、入门指导（包括先决条件、安装、编辑和编译代码的快速指南）以及自动证明搜索功能（Auto）。Safe Agda功能通过--safe选项禁用可能导致不一致的特性，如postulate、--allow-unsolved-metas、--no-positivity-check等。文档还涵盖了文档编写（使用reStructuredText格式）、代码示例类型检查、错误处理、编译Agda程序的方法以及已知问题，例如标准库使用不安全特性导致--safe选项无法成功类型检查。

AI总结

Agda 用户手册 v2.5.4.1 主要介绍了 Agda 编程语言及其相关工具。手册仍在完善中，欢迎通过 GitHub 贡献。

**核心内容**

* **语言参考**：涵盖抽象定义、内建类型、余归纳、余模式、核心语言、数据类型、外部函数接口、函数定义与类型、隐式/实例参数、无关性、Lambda 抽象、局部定义、词法结构、字面量重载、混缀运算符、模块系统、相互递归、模式同义词、积极性检查、假设、编译指令、记录类型、反射、重写、安全 Agda、大小类型、语法糖、望远镜、终止性检查、宇宙层次、With 抽象、Without K 等。
* **工具与使用**：
* **编辑与编译**：提供 Emacs 交互模式，支持类型检查、编译（生成可执行文件）和批处理命令 `agda`。
* **自动证明搜索 (Auto)**：通过 `c-c c-a` 调用，可搜索类型居民并填充目标，支持设置超时、使用 case-split、反证目标及使用定义作为提示。
* **文档编写**：使用 reStructuredText 格式，支持 `.lagda.rst` 文件以进行类型检查。可本地渲染为 HTML 或 LaTeX/PDF。
* **安全模式 (--safe)**：禁用可能导致不一致的特性，如 `postulate`、`--no-positivity-check`、`--no-termination-check`、`--type-in-type`、`--rewriting` 等。注意：标准库因大量使用不安全特性，目前无法在 `--safe` 下通过类型检查。

**重要信息**

* 手册是**进行中的工作**，不完整。
* 自动证明搜索工具名为 Agsy，其所有解都会经过 Agda 检查。
* 文档中的代码示例可通过 `.lagda.rst` 扩展名进行类型检查。
* `--safe` 选项的编译指令 `{-# OPTIONS --safe #-}` 存在已知 bug，可能无法正确传递到导入的文件，建议仅使用命令行选项。