1.	はじめに（Introduction）
2.	エラボレーションとコンパイル（Elaboration and Compilation）
3.	Lean 言語について（The Lean Language）
4.	Terms
5.	Monads and `do`-Notation
6.	IO
7.	タクティクによる証明（Tactic Proofs）
8.	単純化器（The Simplifier）
9.	基本的な型（Basic Types）
10.	Standard Library
11.	Notations and Macros
12.	Output from Lean
13.	Elan
14.	Lake and Reservoir
	Index
15.	この翻訳について

14. Lake and Reservoir

14.1.	Lake
14.2.	Reservoir

14. Lake and Reservoir🔗