←
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.
この翻訳について
4.
ソースファイル(Source Files)
4.1.
ファイル(Files)
4.2.
モジュールの内容(Module Contents)
4.3.
Axioms
4.4.
Attributes
4.5.
Dynamic Typing
4.6.
Coercions
Source Code
Report Issues
4. ソースファイル(Source Files)
4.1.
ファイル(Files)
4.1.1.
モジュール(Modules)
4.1.1.1.
エンコードと表現(Encoding and Representation)
4.1.1.2.
具体的な構文(Concrete Syntax)
4.1.1.2.1.
空白(Whitespace)
4.1.1.2.2.
コメント(Comments)
4.1.1.2.3.
キーワードと識別子(Keywords and Identifiers)
4.1.1.3.
構造体(Structure)
4.1.1.3.1.
モジュールヘッダ(Module Headers)
4.1.1.3.2.
コマンド(Commands)
4.1.1.4.
内容(Contents)
4.1.2.
パッケージ・ライブラリ・ターゲット(Packages, Libraries, and Targets)
4.2.
モジュールの内容(Module Contents)
4.2.1.
コマンドと宣言(Commands and Declaration)
4.2.1.1.
定義に類するコマンド(Definition-Like Commands)
4.2.1.2.
Modifiers
4.2.1.3.
Signatures
4.2.1.4.
ヘッダ(Headers)
4.2.2.
Namespaces
4.2.3.
セクションスコープ(Section Scopes)
4.2.3.1.
セクションスコープの制御(Controlling Section Scopes)
4.2.3.2.
セクション変数(Section Variables)
4.2.3.3.
スコープ属性(Scoped Attributes)
4.3.
Axioms
4.4.
Attributes
4.5.
Dynamic Typing
4.6.
Coercions