Agda User Manual v2.5.4.2

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

摘要

该文档是Agda编程语言用户手册v2.5.4.2版本，由Agda团队于2018年10月29日发布。手册涵盖语言概述、入门指南（包括先决条件、安装步骤、编辑/类型检查/编译快速指南）、语言参考（涵盖抽象定义、内置函数、余归纳、协模式、核心语言、数据类型、外部函数接口、函数定义、函数类型、隐式参数、实例参数、无关性、Lambda抽象、局部定义、词法结构、字面量重载、混合运算符、模块系统、互递归、模式同义词、正性检查、公设、编译指示、记录类型、反射、重写、安全Agda、大小类型、语法糖等30余个主题）、工具（自动证明搜索、命令行选项、编译器、Emacs模式、文学编程、HTML生成、LaTeX生成、库管理）以及贡献指南和许可证信息。文档强调其仍在完善中，欢迎贡献。

AI总结

这是《Agda用户手册 v2.5.4.2》的内容总结。

该手册是Agda编程语言及其类型检查、编译和编辑系统的指南，目前仍在完善中。

**核心内容概述**

1. **入门指南**：介绍了安装Agda的多种方式，包括从Hackage、源码或使用Nix/Homebrew安装，并列举了`cpphs`、`debug`等安装标志。文档强调使用Emacs或Atom编辑器进行交互式开发，核心操作包括加载文件（`C-c C-l`）、查看目标类型（`C-c C-,`）和填充代码（`C-c C-SPC`）。

2. **语言参考**：手册的主体部分，详细说明了Agda语言的各项特性，涵盖抽象定义、内建类型、余归纳、协模式、数据类型、函数定义、隐式参数、实例参数、模块系统、互递归、模式同义词、终止检查、宇宙层级、With-抽象等30多个专题。

3. **工具**：介绍了与Agda配套的工具，包括自动证明搜索（Auto）、命令行选项、编译器、Emacs模式、文学编程支持，以及生成HTML和LaTeX文档的方法。文档还特别说明了如何通过`agda --latex`命令和`postprocess-latex.pl`脚本半自动地排版内联代码。

4. **贡献与许可**：鼓励用户通过Github提交拉取请求或问题来贡献文档。Agda 2采用MIT许可证，其核心开发者包括Ulf Norell、Andreas Abel、Jesper Cockx等人，并列举了众多贡献者。