Agda User Manual v2.6.2

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

摘要

该文档是Agda编程语言用户手册v2.6.2，介绍了Agda的编程语言、类型检查、编译和编辑系统及相关资源。手册内容包括概述、入门指南（如安装、Hello World示例、依赖类型编程）、语言参考（涵盖抽象定义、内置函数、共归纳、模式匹配、覆盖检查、立方体类型、数据类型、函数定义、隐式参数、模块系统等）、工具（如自动证明搜索、命令行选项、编译器、Emacs模式、文字编程、HTML/LaTeX生成、库管理）以及贡献指南。文档强调手册仍在完善中，欢迎通过GitHub贡献。代码示例需遵循特定语法规则以确保可见性和类型正确性。

AI总结

《Agda用户手册v2.6.2》是一份仍在完善中的文档，欢迎通过GitHub提交贡献。手册涵盖了Agda编程语言的核心内容，包括类型检查、编译、编辑系统及相关工具。

**核心内容结构：**

1. **概述与入门**：介绍Agda是什么（依赖类型语言），提供安装指南（源码安装、预编译包）、"Hello world"示例及依赖类型编程入门（如向量、证明加法结合律）。推荐新手先阅读Agda Wiki上的教程和入门章节，而非直接看语言参考。

2. **语言参考**：详细描述Agda语言特性，包括抽象定义、内置类型、共归纳、协模式、核心语言、覆盖检查、立方类型、数据类型、外部函数接口、函数定义、隐式参数、实例参数、不可相关性、Lambda抽象、局部定义、词法结构、运算符重载、模块系统、互递归、模式同义词、积极性检查、公设、编译指令、命题类型、记录类型、反射、重写、运行时无关性、安全Agda、大小类型、排序系统、语法糖、语法声明、望远镜、终止检查、宇宙级别、With抽象、Without K等。

3. **工具**：涵盖自动证明搜索（Auto）、命令行选项、编译器、Emacs模式、文学编程、生成HTML/LaTeX、接口文件、库管理、性能调试、作用域内定义搜索。

4. **文档贡献指南**：说明如何编写文档（使用`.lagda.rst`扩展名）、在Emacs中交互编辑、通过`make user-manual-test`检查代码类型正确性，并强调提交前需用`fix-agda-whitespace`清理尾随空格。

5. **命令行选项**：列出重要选项，如`--help`查看帮助、`--interaction`用于Emacs模式、`--interaction-json`用于Atom等编辑器、`--no-projection-like`关闭投影优化（调试用）、`--only-scope-checking`仅作用域检查、`--version`显示版本。还包含错误与警告控制（如`--allow-incomplete-matches`、`--allow-unsolved-metas`、`--no-positivity-check`、`--no-termination-check`）、模式匹配与等式选项（如`--exact-split`、`--no-eta-equality`）。

6. **教程与资源**：列出相关书籍（如《Programming Languages Foundations in Agda》）、教程笔记（如Jesper Cockx的《Programming and Proving in Agda》）、视频及课程信息，并提醒部分材料可能针对旧版Agda。