Agda User Manual v2.6.3

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

摘要

The Agda User Manual v2.6.3 is an incomplete but comprehensive guide to the Agda programming language, its type checking, compilation system, and related tools. It provides an overview of the language reference, including experimental features like Cubical Agda, copatterns, and guarded recursion. The manual also details various options for type checking, compilation, and system configuration, such as universe levels, Sized Types, and rewrite rules. Users are encouraged to contribute to the manual through GitHub, and additional resources, including tutorials and documentation, are available on the Agda Wiki. The manual covers installation, basic usage, and advanced features while emphasizing the importance of community contributions for its improvement.

AI总结

《Agda User Manual v2.6.3》中文总结

本文档是Agda编程语言的用户手册，涵盖了Agda的类型检查、编译和编辑系统，以及相关资源和工具。以下是文档的主要内容总结：

一、概述
1. Agda是一个功能强大的依赖类型编程语言，支持类型检查、编译和编辑系统。
2. 本手册仍在完善中，欢迎通过GitHub提交更改或修正。
3. 新手应参考Agda Wiki上的资源和“Getting Started”章节，而非直接阅读“Language Reference”。

二、核心功能选项
1. --copatterns (默认启用)：支持通过模式匹配进行协程序定义。
2. --postfix-projections (默认启用)：启用后缀投影表示法。
3. --allow-exec：允许在类型检查期间执行系统调用。
4. --confluence-check：启用全局或局部同余规则检验。
5. --cubical：启用立方体类型（Cubical Agda），并禁用K规则。
6. --erased-cubical：启用一种变体的Cubical Agda，并禁用K规则。
7. --experimental-irrelevance：启用潜在不安全的无关性特性。
8. --guarded：启用保护递归锁和刻度。
9. --injective-type-constructors：启用注入型类型构造函数。
10. --prop：启用或禁用证明不相关的命题声明和使用。
11. --rewriting：启用REWRITE规则声明和使用。

三、错误与警告选项
1. --allow-incomplete-matches：允许不完整的匹配定义并生成接口文件。
2. --allow-unsolved-metas：允许存在未解元变量并生成接口文件。
3. --no-positivity-check：抑制不严格正数据类型的警告。
4. --no-termination-check：抑制可能非终止代码的警告。
5. --warning：设置警告组或标志。

四、模式匹配与相等性选项
1. --exact-split：严格拆分（必要于Cubical Agda）。
2. --keep-pattern-variables：防止交互式情况分割替换变量为点模式。

五、搜索深度与实例选项
1. --instance-search-depth：设置实例搜索深度（默认500）。
2. --inversion-max-depth：设置模式匹配反转最大深度（默认50）。
3. --termination-depth：允许终止检查器计数递减/递增（默认1）。

六、其他特性选项
1. --double-check：双重检查所有项（默认关闭）。
2. --no-double-check：关闭双重检查（默认启用）。
3. --guardedness：启用/禁用构造型保护协程序（与sized types不兼容）。
4. --irrelevant-projections：启用/禁用无关记录字段的投影（可能导致不一致）。
5. --auto-inline：启用自动内联（默认关闭）。
6. --no-auto-inline：禁用自动内联（默认启用）。
7. --no-fast-reduce：禁用Agda抽象机的还原。
8. --call-by-name：关闭Agda抽象机的按需调用。
9. --no-forcing：禁用强制优化（从2.6.1起作为pragma选项）。
10. --no-print-pattern-synonyms：始终展开模式同义词。
11. --no-syntactic-equality：禁用语法相等性快捷方式。
12. --syntactic-equality：为语法相等性快捷方式分配单位（实验功能）。
13. --safe：禁用postulates和不安全OPTIONS pragma，防止同时使用sized types和guardedness。
14. --sized-types：启用/禁用sized types（与guardedness不兼容）。
15. --no-import-sorts：禁用隐式导入Agda.Primitive模块。
16. --no-load-primitives：不加载primitive模块（需手动确保加载）。

以上是《Agda User Manual v2.6.3》的核心内容总结，涵盖了语言功能、配置选项及其用途，旨在帮助用户快速理解和使用Agda语言及其工具链。