←Prev ↑Up Next→

The Lean Language Reference 日本語訳

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.	この翻訳について

6. 項（Terms）

6.1.	識別子（Identifiers）
6.2.	関数型（Function Types）
6.3.	関数（Functions）
6.4.	関数適用（Function Application）
6.5.	リテラル（Literals）
6.6.	構造体とコンストラクタ（Structures and Constructors）
6.7.	条件（Conditionals）
6.8.	パターンマッチ（Pattern Matching）
6.9.	ホール（Holes）
6.10.	Type Ascription
6.11.	Quotation と Antiquotation（Quotation and Antiquotation）
6.12.	`do` 記法（`do`-Notation）
6.13.	証明（Proofs）

6.12. do 記法（do-Notation）

Source Code
Report Issues

6.12. `do` 記法（`do`-Notation）

Lean.Parser.Term.do : termdo 記法はモナドの章で説明されています。