Agda User Manual v2.6.2.1

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

摘要

该文档是Agda用户手册v2.6.2.1版，主要介绍了Agda编程语言的命令行选项、功能特性及使用指南。文档详细列出了多个编译选项，如--cubical启用立方体特性、--rewriting启用重写规则、--allow-incomplete-matches允许不完整模式匹配等。同时涵盖了错误与警告管理、模式匹配与等式处理、LaTeX后端排版控制等内容。文档强调用户手册仍在完善中，并提供了Agda Wiki等资源链接供用户参考。此外，还说明了代码示例的语法要求，包括可见性、有效性检查等规范。

AI总结

Agda用户手册v2.6.2.1总结

**核心功能**
- 提供多种编译选项，包括启用立方体特征（`--cubical`）、实验性无关性（`--experimental-irrelevance`）、单射类型构造器（`--injective-type-constructors`）、重写规则（`--rewriting`）以及允许系统调用（`--allow-exec`）。
- 支持错误与警告控制，如允许不完整匹配（`--allow-incomplete-matches`）、未解决元变量（`--allow-unsolved-metas`），并可关闭积极性检查（`--no-positivity-check`）和终止性检查（`--no-termination-check`）。
- 提供模式匹配与等式相关选项，如精确拆分（`--exact-split`）和η-等式（`--no-eta-equality`）。

**文档结构**
- 手册仍在完善中，欢迎通过GitHub贡献。
- 内容涵盖：概述、入门指南、语言参考（抽象定义、内置类型、共归纳、协模式、覆盖检查、立方体、累积性、数据类型、扁平模态、外部函数接口、函数定义、函数类型、变量泛化、守卫立方体、隐式参数、实例参数、无关性、Lambda抽象、局部定义、词法结构、字面量重载、混合固定运算符、模块系统、相互递归、模式同义词、积极性检查、假设、编译指示、Prop、记录类型、反射、重写、运行时无关性、安全Agda、大小类型、排序系统、语法糖、语法声明、望远镜、终止性检查、宇宙层级、With-抽象、Without K）以及工具（自动证明搜索、命令行选项、编译器、Emacs模式、文学编程、生成HTML/LaTeX、接口文件、库管理、性能调试、作用域搜索定义）。

**LaTeX后端与文档编写**
- 支持通过Makefile自动化生成LaTeX文档。
- 可通过重定义`\AgdaFormat`命令控制单个令牌的排版。
- 提供`sed`脚本模拟`%format`规则。
- 文档文件使用`.lagda.rst`扩展名，可在Emacs中交互编辑。
- 通过`make user-manual-test`验证所有代码示例的类型正确性。
- 代码示例分为可见且可检查的、可见但不可检查的、隐藏但可检查的以及隐藏且不可检查的四类。

**关键信息**
- 手册最新PDF版本可从GitHub Actions下载。
- 入门资源推荐访问Agda Wiki。
- 文档编写需注意去除尾部空白（`fix-agda-whitespace`）。