Idris 语言文档 Version 1.3.1

• 语言: 中文（简体）
• 格式: .pdf
• 来源: idris-zh.readthedocs.io

摘要

文档介绍了Idris语言的基础使用和效果系统，包括如何编写和运行第一个Idris程序、命令行选项的使用、交互式环境的操作，以及效果系统中State、StdIO、System等模块的功能。文档还包括了一些代码示例和类型检查的过程。

AI总结

《Idris语言文档 Version 1.3.1》总结如下：

---

### **1. 安装验证**
- 创建一个名为 `hello.idr` 的文件，内容如下：

  module Main
  main : IO ()
  main = putStrLn "Hello world"

- 在命令行中编译并运行程序：

  $ idris hello.idr -o hello
  $ ./hello

输出结果为：`Hello world`。

- 常用命令行选项：
- `-o prog`：编译成名为 `prog` 的可执行文件。
- `--check`：对文件及其依赖进行类型检查。
- `--package pkg`：将包添加为依赖。
- `--help`：显示用法摘要和命令行选项。

---

### **2. 交互式环境**
- 在命令行中输入 `idris` 启动交互式环境，提供类似 `ghci` 的交互界面。
-示例操作：

  $ idris hello.idr
  ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ 
  Version 1.3.1 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ 
  /___/\__,_/_/ /_/____/ Type :? for help

- 交互式操作：
- `:t main`：查看 `main` 的类型。
- `:c hello`：编译程序。
- `:q`：退出交互式环境。

---

### **3. 数据类型与函数**
- **数据类型**：`Nat`、`Int`、`String`、`Bool` 等。
- **函数**：
- `getResources`：获取资源。
- `putStrLn`：输出字符串并换行。

---

### **4. 依赖管理**
- 使用 `--package` 选项管理依赖，例如：

  $ idris --package contrib your_file.idr

---

### **5. 系统模块**
- 提供与系统交互的功能：
- `getArgs`：获取命令行参数。
- `time`：获取当前时间（以整数表示）。
- `getEnv`：获取环境变量。

---

### **6. 效果系统**
- 支持多种效果（Effects）：
- **状态（STATE**)：
- `get`：获取状态。
- `put`：更新状态。
- **随机数（RND**)：
- `srand`：设置随机种子。
- `rndInt`：生成整数范围内的随机数。
- **选择（SELECT**)：
- `select`：从列表中选择一个元素。
- **标准IO（STDIO**)：
- `putChar`、`putStr`、`putStrLn`：输出字符、字符串或换行字符串。
- `getStr`、`getChar`：读取输入。

---

### **7. 定理证明工具**
- 交互式定理证明工具支持以下命令：
- `intros`：引入假设。
- `induction`：使用归纳法证明。
- `compute`：计算表达式。
- `trivial`：用于简单的证明。
- `applicateThese`：应用多个引理。

---

### **8. 其他工具和资源**
- 提供多种教程和参考文档，包括：
- 系统教程。
- 常见问题解答（FAQ）。
- 语言参考。
- 效果系统教程。

---

### **9. 版权声明**
- 文档以 Creative Commons Attribution-ShareAlike 4.0 International License 授权发布。

---

以上为《Idris语言文档 Version 1.3.1》的核心内容总结。