Docs

モジュールにドキュメントを書ける

data Elem : Vect n Ty -> Ty -> Type

型文脈での場所を指す

Here : Elem (t :: ts) t

There : Elem ts t -> Elem (t' :: ts) t

MkYummy : (food : String) -> Yummy

Yummyを作る

food

食べるもの

data Partial : Type -> Type

A computation that may someday finish

Now : (value : a) -> Partial a

A finished computation

value

the result

Later : (rest : Delayed Infinite (Partial a)) -> Partial a

A not-yet-finished computation

rest

the remaining work

data Term : (ctxt : Vect n Ty) -> (ty : Ty) -> Type

もうちょっと面白いデータ型

n

自由変数の数

ctxt

自由変数の型文脈

ty

項の型

UnitCon : Term ctxt UNIT

Unit型のコンストラクタ
もっとコメント

ctxt

型文脈

App : (f : Term ctxt (ARR t1 t2)) -> (x : Term ctxt t1) -> Term ctxt t2

関数適用

f

適用する関数

x

引数

Lam : (body : Term (t1 :: ctxt) t2) -> Term ctxt (ARR t1 t2)

ラムダ抽象

body

関数本体

Var : (i : Elem ctxt t) -> Term ctxt t

変数

i

de Bruijn インデックス

data Ty : Type

シンプルなデータ型

UNIT : Ty

Unit型

ARR : Ty -> Ty -> Ty

関数型

record Yummy 

フィールドやコンストラクタを含めてレコードにもドキュメントが書けるよ

MkYummy : (food : String) -> Yummy

Yummyを作る

food

食べるもの

food : (rec : Yummy) -> String

食べるもの

add : (n : Nat) -> (m : Nat) -> Nat

数値を足す

足し算はめちゃくちゃすごいよね。この段落はOverviewに含まれない。
後続の行も1つの段落に入る。

ドキュメント内に表示されるコードサンプルを書くこともできる

add 4 5

リスト記法：

• はい
• いいえ
• コードの add や 太字 なども使える

n

は再帰パラメータ

m

は再帰パラメータでない

appendV : (xs : Vect n a) -> (ys : Vect m a) -> Vect (add n m) a

ベクタを連結する

a

ベクタの内容

xs

先頭のベクタ（再帰引数）

ys

次のベクタ（場合分けに使われない）