Agda User Manual v2.6.2.1

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

摘要

文档是Agda 2.6.2.1的用户手册，系统介绍了Agda编程语言及其相关工具和资源的使用。手册涵盖了命令行选项、编程语法、代码示例、错误处理以及高级功能如Cubical和HTML/LaTeX生成。Agda手册旨在帮助用户理解和使用Agda语言，提供了详细的使用说明和故障排除指南，强调了命令行选项的重要性以及如何优化代码的编写和调试。

AI总结

《Agda User Manual v2.6.2.1》文档内容总结如下：

1. **命令行选项**：
- **一般选项**：
- `--help`: 显示帮助信息或指定主题的帮助。
- `--interaction` 和 `--interaction-json`:用于与Emacs或其他编辑器（如Atom）配合使用。
- `--version`: 显示版本号。
- `--print-agda-dir`: 显示Agda目录。
- **错误和警告**：
- `--allow-incomplete-matches`:允许不完整的模式匹配定义。
- `--allow-unsolved-metas`:允许未解决的元变量。
- `--no-positivity-check`:不警告不严格正定的数据类型。
- `--no-termination-check`:不警告可能非终止的代码。
- **模式匹配与相等性**：
- `--exact-split` 和 `--no-exact-split`:控制定义中的子句是否必须作为定义等式，除非标记为CATCHALL。
- `--no-eta-equality`:禁用eta等式。
- **其他选项**：
- `--cubical`:启用立方体特性。
- `--experimental-irrelevance`:启用可能不安全的无关紧要特性。
- `--injective-type-constructors$:启用注入型构造函数，使Agda反经典且可能不一致。
- `--rewriting`:启用REWRITE规则的声明和使用。

2. **生成LaTeX文件**：
- 使用`agda --latex {file}.lagda`生成TeX文件，然后使用pdflatex、xelatex或lualatex编译。
- 需要在源文件中导入LaTeX包`agda.sty`，可通过覆盖其定义来自定义代码样式。
- 注意Unicode字符可能需要额外的配置，如使用`inputenc`包。

3. **文档编写与代码示例**：
- 代码示例应尽量可见且有效，Agda会自动检查其正确性。
- 使用`::`语法嵌入代码示例。
- 在Emacs中，可使用`agda2-mode`和`rst-mode`切换编辑模式。
- 提交文档前需运行`fix-agda-whitespace`去除多余空白字符。

4. **资源与贡献**：
- Agda Wiki提供大量资源，包括教程、文档等。
- 文档是正在完善的，欢迎通过GitHub提Pull Request或Issue进行贡献。
- 最新PDF版手册可从GitHub Actions获取。

本文档涵盖了Agda编程语言的核心功能、命令行选项、工具使用及文档编写规范等内容，旨在为用户提供全面而易懂的使用指南。