为 Idris 代码添加文档
Idris 文档主要有两种形式：注释（comments）和内联 API 文档（inline API documentation）。注释仅供阅读者参考，编译器会忽略；内联 API 文档则会被编译器解析并存储，供后续查阅。要查看某个声明 f 的文档，可在 REPL 中输入 :doc f，或在编辑器中使用相应命令（如 Emacs 的 C-c C-d，Vim 的 <LocalLeader>h）。
内联文档（Inline Documentation）
Idris 还支持丰富的内联文档语法。你可以为类型签名中的具名参数和变量单独添加注释，其语法类似于 Javadoc 的参数注释。
文档注释总是位于所注释声明的前面。内联文档既可用于顶层声明，也可用于构造子（constructor）。对于构造子、类型构造子或函数的特定参数，可以通过参数名为其单独添加文档说明。
声明的内联文档由一串连续的行组成，每行都以 |||`（三个竖线）开头。文档的第一段被视为概述，在某些场景下只会显示这部分内容。在整体文档之后，还可以为特定具名参数添加说明，这些参数可以是显式命名的，也可以是自由变量转为隐式参数的结果。注释语法与 Javadoc 注释类似，例如对于具名参数 `(n : T)，对应的注释为 ||| @ n 描述内容，并放在声明之前。
文档内容采用 Markdown 语法编写，但并非所有场景都能完整显示所有格式（例如在 REPL 查看文档时不会显示图片，只有部分终端能正确渲染斜体）。下方给出了一组完整的示例。
||| Modules can also be documented.
module Docs
||| Add some numbers.
|||
||| Addition is really great. This paragraph is not part of the overview.
||| Still the same paragraph.
|||
||| You can even provide examples which are inlined in the documentation:
||| ```idris example
||| add 4 5
||| ```
|||
||| Lists are also nifty:
||| * Really nifty!
||| * Yep!
||| * The name `add` is a **bold** choice
||| @ n is the recursive param
||| @ m is not
add : (n, m : Nat) -> Nat
add Z m = m
add (S n) m = S (add n m)
||| Append some vectors
||| @ a the contents of the vectors
||| @ xs the first vector (recursive param)
||| @ ys the second vector (not analysed)
appendV : (xs : Vect n a) -> (ys : Vect m a) -> Vect (add n m) a
appendV [] ys = ys
appendV (x::xs) ys = x :: appendV xs ys
||| Here's a simple datatype
data Ty =
||| Unit
UNIT |
||| Functions
ARR Ty Ty
||| Points to a place in a typing context
data Elem : Vect n Ty -> Ty -> Type where
Here : {ts : Vect n Ty} -> Elem (t::ts) t
There : {ts : Vect n Ty} -> Elem ts t -> Elem (t'::ts) t
||| A more interesting datatype
||| @ n the number of free variables
||| @ ctxt a typing context for the free variables
||| @ ty the type of the term
data Term : (ctxt : Vect n Ty) -> (ty : Ty) -> Type where
||| The constructor of the unit type
||| More comment
||| @ ctxt the typing context
UnitCon : {ctxt : Vect n Ty} -> Term ctxt UNIT
||| Function application
||| @ f the function to apply
||| @ x the argument
App : {ctxt : Vect n Ty} -> (f : Term ctxt (ARR t1 t2)) -> (x : Term ctxt t1) -> Term ctxt t2
||| Lambda
||| @ body the function body
Lam : {ctxt : Vect n Ty} -> (body : Term (t1::ctxt) t2) -> Term ctxt (ARR t1 t2)
||| Variables
||| @ i de Bruijn index
Var : {ctxt : Vect n Ty} -> (i : Elem ctxt t) -> Term ctxt t
||| We can document records, including their fields and constructors
record Yummy where
||| Make a yummy
constructor MkYummy
||| What to eat
food : String
注释
使用注释来解释代码为何如此编写。Idris 的注释语法与 Haskell 相同：以 -- 开头的行是单行注释，用 {- 和 -} 括起来的区域是多行注释。这些注释可用于注释掉代码行，或为 Idris 代码的读者提供简单的文档说明。