Agda User Manual v2.6.4.2
1.38 MB
311 页
0 评论
语言 | 格式 | 评分 |
---|---|---|
英语 | .pdf | 3 |
摘要 | ||
文档主要介绍了Agda 2.6.4.2版本的用户手册,涵盖了命令行选项的使用、性能优化选项、编译与库的相关配置以及如何为Agda贡献力量。手册详细说明了各种命令行标志的功能,如--termination-check、--exact-split、--cohesion等,适用于不同的编译和类型检查场景。此外,还提供了如何编译Agda代码、设置编译器路径及库目录的指南,帮助用户更好地使用Agda进行开发和文档编写。 | ||
AI总结 | ||
《Agda User Manual v2.6.4.2》详细介绍了Agda编程语言及相关工具和资源的使用方法。以下是文档内容的总结:
---
### 1. 命令行选项
文档详细列举了Agda的命令行选项,包括:
- **终止检查**:启用或禁用终止检查默认启用,--no-termination-check禁用。
- **警告设置**:设置警告组或标志,-W {GROUP|FLAG}。
- **模式匹配与等效性**:
- --exact-split:要求定义中的所有子句都作为定义等式。
- --hidden-argument-puns:启用隐藏参数匹配,默认禁用。
- --no-eta-equality:默认禁用 eta 展开等式,--eta-equality启用。
- **凝聚模式**:启用或禁用凝聚模式,--cohesion启用,--no-cohesion禁用,默认禁用。
- **模式匹配优化**:--flat-split启用在@♭参数上的模式匹配。
- **模式匹配禁用**:--no-pattern-matching禁用模式匹配,--pattern-matching启用。
### 2. 处理与编译选项
- **编译目录设置**:--compile-dir设定编译输出目录。
- **主模块设置**:--no-main不将当前模块视为主模块,--main默认启用。
- **编译器路径**:--with-compiler设定编译器路径,GHC为默认。
- **库文件使用**:--no-default-libraries不使用默认库文件,--no-libraries禁用所有库文件,--no-interfaces禁用接口文件,--generate-interfaces生成接口文件。
### 3. 性能优化选项
- **自动内联**:--auto-inline启用自动内联,--no-auto-inline禁用,前者默认。
- **缓存类型检查**:--caching启用缓存,默认。
- **调用策略**:--call-by-name禁用询问式需要评估,--no-call-by-name默认启用。
- **强制优化**:--no-forcing禁用强制优化,--forcing启用,默认。
### 4. 其他选项
- **辅助工具**:显示版本号、Agda配置目录。
- **编码转换**:将无法显示的字符转换为其他字符。
- **umbra模式**:避免在某些环境中使用中文提示。
### 5. 文档贡献
Agda文档欢迎社区贡献,可在GitHub上fork仓库并提交Pull Request。本地渲染文档需要Python、Sphinx和LaTeX等,使用Make生成HTML文档。
---
该手册详细介绍了Agda的功能及其选项,帮助用户高效使用和贡献Agda生态系统。 |
P1
P2
P3
P4
P5
P6
P7
下载文档到本地,方便使用
- 可预览页数已用完,剩余
304 页请下载阅读 -
文档评分