Agda User Manual v2.5.4.2

### 《Agda User Manual v2.5.4.2》内容总结 Agda用户手册主要介绍了Agda编程语言及其工具的使用方法，以下是核心内容的总结： --- #### 1. **生成LaTeX** - Agda支持通过 `.lagda` 文件生成LaTeX文档。 - 码块需使用 `\begin{code}` 和 `\end{code}` 包裹，示例： ```tex \begin{document} Introduction \begin{code} module MyPaper where open import Prelude five : Nat five = 2 + 3 \end{code} \end{document} ``` - 支持生成HTML文档，并可通过 `make user-manual-test` 检查代码示例的正确性。 --- #### 2. **库管理** - Agda有一个简单的包管理系统，支持多个库的管理。 - 使用标准库时需： 1. 创建 `AGDA_DIR/libraries` 文件，内容为 `AGDA_STDLIB/standard-library.agda-lib`。 2. 创建 `AGDA_DIR/defaults` 文件，内容为 `standard-library`。 - 默认库路径： - Unix-like系统：`~/.agda`。 - Windows：`C:\Users\USERNAME\AppData\Roaming\agda`。 --- #### 3. **代码编辑与类型检查** - 支持批处理模式命令行工具 `agda`，可通过 `agda --help` 查看帮助。 - Agda文件可以包含代码示例，需通过 `agda2-mode` 和 `rst-mode` 提供的交互模式类型检查。 - 在 `.lagda.rst` 文件中嵌入代码示例时，需确保代码正确，避免尾随空格。 --- #### 4. **外部函数接口 (FFI)** - 支持将Haskell类型映射到Agda类型，使用 `FOREIGN` 和 `COMPILE` pragmas。 - 非透明类型： ```haskell postulate FileHandle : Set {-# COMPILE GHC FileHandle = type System.IO.Handle #-} ``` - 透明数据类型： ```haskell data Maybe (A : Set) : Set where nothing | just {-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-} ``` - 内置类型映射： - `NAT` → `Integer`。 - `STRING` → `Data.Text.Text`。 - `FLOAT` → `Double`。 --- #### 5. **编译器** - **GHC后端**：将Agda代码编译为Haskell代码，使用 `agda --compile` 命令。 - 示例： ```agda module HelloWorld where postulate putStrLn : String → IO {-# COMPILE GHC putStrLn = Text.putStrLn #-} main : IO main = putStrLn "Hello, World!" ``` - 需要额外库支持： - `primFloatEquality` 需要 `ieee754` 库。 - **JavaScript后端**：将Agda代码编译为JavaScript代码。 --- #### 6. **其他** - Agda是布局敏感语言，使用与Haskell类似的缩进规则，但不允许使用 `{}` 和 `;`。 - 支持逐字编程（Literate Programming），文件扩展名为 `.lagda`。 - 手册为工作版本，欢迎通过GitHub提出修改和补充。 --- 以上为手册的核心内容，涵盖了Agda的库管理、文档生成、类型检查、外部函数接口及编译器的主要功能。