Cross-Reference Redirection

←Prev↑UpNext→

1.	はじめに（Introduction）
2.	エラボレーションとコンパイル（Elaboration and Compilation）
3.	型システム（The Type System）
4.	ソースファイル（Source Files）
5.	再帰定義（Recursive Definitions）
6.	項（Terms）
7.	型クラス（Type Classes）
8.	関手・モナド・do記法（Functors, Monads and `do`-Notation）
9.	IO
10.	タクティクによる証明（Tactic Proofs）
11.	単純化器（The Simplifier）
12.	基本的な型（Basic Types）
13.	Standard Library
14.	記法とマクロ（Notations and Macros）
15.	Output from Lean
16.	Elan
17.	Lake and Reservoir
	Index
18.	この翻訳について