Agda User Manual v2.6.3

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

摘要

本文档是Agda 2.6.3版本的用户手册，介绍了Agda编程语言及其类型检查、编译和编辑系统。手册包含概述、入门指南、语言参考、工具和文档编写等内容。概述指出手册仍在完善中，鼓励贡献。入门指南介绍了Agda的依赖类型特性、安装方法、Hello World示例和教程列表。语言参考涵盖抽象定义、内置类型、共归纳、协模式、核心语言、覆盖检查、立方类型、数据类型、函数定义等众多特性。文档编写部分说明了使用reStructuredText格式，通过.lagda.rst扩展名可使Agda识别并类型检查代码示例，还提供了本地构建文档和类型检查代码示例的方法。

AI总结

该文档是《Agda 用户手册 v2.6.3》的概述，主要内容包括：

- **手册状态**：仍在完善中，欢迎通过 GitHub 提交贡献。
- **内容结构**：涵盖 Agda 语言参考、类型检查、编译系统及相关工具。建议新手从“入门”章节开始。
- **文档格式**：使用 reStructuredText 编写，支持 `.lagda.rst` 扩展名，可嵌入并自动类型检查 Agda 代码示例。
- **本地构建**：需安装 Python、Sphinx、ImageMagick、LaTeX 等依赖，可通过 `make html` 生成 HTML 文档。
- **代码示例**：分为可见且可检查、仅可见、仅可检查三类，推荐使用“可见且可检查”形式。
- **命令行选项**：包括启用实验性功能（如 Cubical、Guarded、Rewriting）、控制错误与警告、设置编译目录、生成高亮代码等。
- **测试与提交**：可通过 `make user-manual-test` 检查所有代码示例正确性，提交前需运行 `fix-agda-whitespace` 清理空格。