Agda User Manual v2.6.1.2

《Agda User Manual v2.6.1.2》是Agda编程语言的用户手册，以下是对其内容的简要总结： 1. **概述** - Agda是一种依赖类型编程语言，getExtension of Martin-Löf type theory，可用于编程和数学证明。 - 手册仍在完善中，欢迎通过GitHub贡献内容。 - 新手应参考“Getting Started”章节和Agda Wiki上的资源。 2. **入门** - Agda基于类型理论，支持强类型和依赖类型，适合作为证明助手。 - 依赖类型的核心特点是类型系统中可以嵌入逻辑信息。 3. **语言参考** - 介绍了Agda的内置类型（如自然数、布尔值、字符串等）和高级特性。 - 内置类型通过BUILTIN pragmas绑定，可以使用primitive函数。 - 包括模式同名（pattern synonyms）、正确定性检查（positivity checking）等高级功能。 4. **工具** - 提供命令行选项（如--compile）和多个编译器后端（GHC、JavaScript）。 - 示例：通过GHC后端将Agda程序编译为Haskell程序，支持Foreign Function Interface。 5. **贡献** - Agda项目及相关库托管于GitHub，欢迎贡献代码和文档。 - 文档使用reStructuredText格式，可本地渲染或发布至readthedocs。 总结：Agda用户手册全面介绍了语言特性、工具使用和贡献指南，是学习Agda的重要参考资料。