Agda User Manual v2.6.2.2

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

摘要

本文档是Agda编程语言用户手册v2.6.2.2，介绍了Agda的类型检查、编译和编辑系统及相关工具。文档包括概述、入门指南、语言参考、工具章节以及文档编写说明。入门部分涵盖Agda定义、安装、Hello World示例和教程列表。语言参考详细描述了抽象定义、内置类型、共归纳、协模式、核心语言、覆盖检查、立方类型、累积性、数据类型、函数定义、模块系统等特性。工具章节说明了命令行选项，如--help、--interaction、--version等。文档还介绍了如何编写文档，包括使用.lagda.rst扩展名嵌入代码示例，以及通过Sphinx和sphinx-rtd-theme在本地渲染文档。文档强调贡献和修正的欢迎，并提供了GitHub链接和许可证信息。

AI总结

该文档是《Agda用户手册 v2.6.2.2》的目录及部分内容摘要。核心内容如下：

- **手册性质**：该手册仍在完善中，欢迎通过GitHub贡献。主要介绍Agda编程语言及其类型检查、编译、编辑系统和相关工具。
- **文档结构**：手册包含“概述”、“入门指南”（推荐新手阅读）、“语言参考”（语言描述）和“工具”（编辑与编译系统）等章节。
- **文档格式**：文档使用reStructuredText格式编写，可通过Sphinx构建为HTML或PDF。代码示例需嵌入在`.lagda.rst`文件中，以便Agda进行类型检查。
- **代码示例**：文档中的代码示例分为“可见且可检查”（用户可见且会被Agda验证）和“不可见或不可检查”两类。
- **命令行选项**：手册列出了大量命令行选项，例如`--help`（帮助）、`--interaction`（Emacs模式）、`--cubical`、`--no-projection-like`（调试用）等，用于控制Agda的行为。
- **其他**：手册末尾提供了详细的索引，列出了所有命令行选项和符号。