Agda User Manual v2.6.1

以下是对《Agda User Manual v2.6.1》文档内容的简要总结，重点突出核心观点和关键信息，逻辑连贯，语言简洁明了： --- ### 《Agda User Manual v2.6.1》总结 #### 1. **手册概述** - 本手册是Agda编程语言及其相关工具的官方文档，目前仍在完善中，欢迎贡献。 - 可从GitHub Actions下载最新PDF版本，或访问Agda Wiki获取更多资源（如教程、文档等）。 #### 2. **Agda简介** - Agda是一种基于类型的编程语言，支持类型检查、编译和编辑系统。 - 适合新手的资源包括Agda Wiki和“Getting Started”章节。 - 语言参考章节详细描述了Agda语言的语法和核心功能。 #### 3. **主要功能** - **类型检查与编译**：支持类型推导、模式匹配、依赖类型等。 - **高级特性**： - Coinduction（共归纳）、Copatterns（协模式）、Cubical（立方体类型理论）。 - Cumulativity（累加性）、Data Types（数据类型）、Flat Modality（模态）等。 - **工具与资源**： - Foreign Function Interface（FFI，外部函数接口）。 - 模块系统、互归归、模式同义词等功能。 - 支持隐式参数、局部定义和字面过载。 #### 4. **新功能（版本2.6.1）** - `--allow-incomplete-matches`：允许不完全匹配的模式匹配定义。 - `--allow-unsolved-metas`：允许未解元变量。 - `--no-flat-split`：禁用@♭参数上的模式匹配。 - 新增`--interaction-json`选项，支持与其他编辑器（如Atom）交互。 #### 5. **命令行选项** - **一般选项**： - `--help`：显示帮助信息。 - `--interaction`：与Emacs模式配合使用。 - `--version`：显示版本号。 - **类型检查与编译**： - `--only-scope-checking`：仅执行作用域检查。 - `--no-positivity-check`：禁用严格正定性检查。 - **模式匹配与等式**： - `--exact-split`：要求所有定义子句作为定义等式。 - `--no-eta-equality`：默认禁用Eta等同性。 - **打印与调试**： - `--no-unicode`：不使用Unicode字符显示。 - `--show-implicit`：显示隐式参数。 - **实验性功能**： - `--confluence-check`：启用REWRITE规则的可合流性检查。 - `--cubical`：启用立方体特性。 - `--injective-type-constructors`：启用注入式类型构造。 #### 6. **文档与贡献** - 使用`.lagda.rst`扩展名的文档文件会被Agda识别并类型检查。 - 文档中的代码示例需通过`make user-manual-test`验证。 - 贡献者需通过GitHub fork仓库并提交Pull Request（PR），可参考标签`difficulty: easy`和`help wanted`。 #### 7. **其他工具与资源** - `agda-ghc-names`：将生成的Haskell代码名称映射回Agda名称。 - "Search About"功能（自版本2.5.1起）：在作用域中搜索定义，支持按标识符和子字符串匹配。 --- 以上是《Agda User Manual v2.6.1》的核心内容和关键信息的总结，旨在帮助读者快速了解Agda的主要功能、使用方法和新特性。