3. Lean 言語について（The Lean Language）

  1. 3.1. ファイル（Files）
    1. 3.1.1. モジュール（Modules）
      1. 3.1.1.1. エンコードと表現（Encoding and Representation）
      2. 3.1.1.2. 具体的な構文（Concrete Syntax）
        1. 3.1.1.2.1. 空白（Whitespace）
        2. 3.1.1.2.2. コメント（Comments）
        3. 3.1.1.2.3. キーワードと識別子（Keywords and Identifiers）
      3. 3.1.1.3. 構造体（Structure）
        1. 3.1.1.3.1. モジュールヘッダ（Module Headers）
        2. 3.1.1.3.2. コマンド（Commands）
      4. 3.1.1.4. 内容（Contents）
    2. 3.1.2. パッケージ・ライブラリ・ターゲット（Packages, Libraries, and Targets）
  2. 3.2. 型システム（The Type System）
    1. 3.2.1. 関数（Functions）
      1. 3.2.1.1. 関数（Functions）
      2. 3.2.1.2. カリー化（Currying）
      3. 3.2.1.3. 暗黙の関数（Implicit Functions）
      4. 3.2.1.4. パターンマッチ（Pattern Matching）
      5. 3.2.1.5. 外延性（Extensionality）
      6. 3.2.1.6. 全域性と停止（Totality and Termination）
    2. 3.2.2. 命題（Propositions）
    3. 3.2.3. 宇宙（Universes）
      1. 3.2.3.1. Predicativity
      2. 3.2.3.2. 多相性（Polymorphism）
        1. 3.2.3.2.1. レベル式（Level Expressions）
      3. 3.2.3.3. 宇宙変数の束縛（Universe Variable Bindings）
        1. 3.2.3.3.1. Universe Unification
    4. 3.2.4. 帰納型
      1. 3.2.4.1. 帰納型の宣言
        1. 3.2.4.1.1. パラメータと添字
        2. 3.2.4.1.2. 帰納型の例
        3. 3.2.4.1.3. 匿名コンストラクタ構文
        4. 3.2.4.1.4. インスタンスの導出
      2. 3.2.4.2. 構造体宣言（Structure Declarations）
        1. 3.2.4.2.1. 構造体のパラメータ（Structure Parameters）
        2. 3.2.4.2.2. フィールド（Fields）
        3. 3.2.4.2.3. 構造体のコンストラクタ（Structure Constructors）
        4. 3.2.4.2.4. 構造体の継承（Structure Inheritance）
      3. 3.2.4.3. 論理モデル（Logical Model）
        1. 3.2.4.3.1. 再帰子（Recursors）
          1. 3.2.4.3.1.1. 再帰子の型（Recursor Types）
            1. 3.2.4.3.1.1.1. Subsingleton 除去（Subsingleton Elimination）
          2. 3.2.4.3.1.2. 簡約（Reduction）
        2. 3.2.4.3.2. 適格要件（Well-Formedness Requirements）
          1. 3.2.4.3.2.1. 宇宙レベル（Universe Levels）
          2. 3.2.4.3.2.2. Strict Positivity
          3. 3.2.4.3.2.3. Prop vs Type
        3. 3.2.4.3.3. 停止性チェックのための構成（Constructions for Termination Checking）
      4. 3.2.4.4. ランタイム表現
        1. 3.2.4.4.1. 例外
        2. 3.2.4.4.2. Relevance
        3. 3.2.4.4.3. 自明なラッパ
        4. 3.2.4.4.4. その他の帰納型
          1. 3.2.4.4.4.1. FFI
      5. 3.2.4.5. 相互帰納型
        1. 3.2.4.5.1. 要件
          1. 3.2.4.5.1.1. 相互依存
          2. 3.2.4.5.1.2. マッチすべきパラメータ
          3. 3.2.4.5.1.3. 宇宙レベル
          4. 3.2.4.5.1.4. Positivity
        2. 3.2.4.5.2. 再帰子
        3. 3.2.4.5.3. ランタイム表現
    5. 3.2.5. Quotients
  3. 3.3. モジュールの内容（Module Contents）
    1. 3.3.1. コマンドと宣言（Commands and Declaration）
      1. 3.3.1.1. 定義に類するコマンド（Definition-Like Commands）
      2. 3.3.1.2. Modifiers
      3. 3.3.1.3. Signatures
      4. 3.3.1.4. ヘッダ（Headers）
    2. 3.3.2. Section Scopes
  4. 3.4. Axioms
  5. 3.5. Recursive Definitions
    1. 3.5.1. Structural Recursion
      1. 3.5.1.1. Mutual Structural Recursion
    2. 3.5.2. Well-Founded Recursion
    3. 3.5.3. Controlling Reduction
    4. 3.5.4. Partial and Unsafe Recursive Definitions
  6. 3.6. Attributes
  7. 3.7. Type Classes
    1. 3.7.1. Class Declarations
      1. 3.7.1.1. Sum Types as Classes
      2. 3.7.1.2. Class Abbreviations
    2. 3.7.2. Instance Declarations
      1. 3.7.2.1. Recursive Instances
      2. 3.7.2.2. Instances of class inductives
      3. 3.7.2.3. Instance Priorities
      4. 3.7.2.4. Default Instances
      5. 3.7.2.5. The Instance Attribute
    3. 3.7.3. Instance Synthesis
      1. 3.7.3.1. Instance Search Summary
      2. 3.7.3.2. Instance Search Problems
      3. 3.7.3.3. Candidate Instances
      4. 3.7.3.4. Instance Parameters and Synthesis
      5. 3.7.3.5. Output Parameters
      6. 3.7.3.6. Default Instances
      7. 3.7.3.7. “Morally Canonical” Instances
      8. 3.7.3.8. Options
    4. 3.7.4. Deriving Instances
      1. 3.7.4.1. Deriving Handlers
    5. 3.7.5. Basic Classes
      1. 3.7.5.1. Boolean Equality Tests
      2. 3.7.5.2. Ordering
      3. 3.7.5.3. Decidability
      4. 3.7.5.4. Inhabited Types
      5. 3.7.5.5. Visible Representations
      6. 3.7.5.6. Arithmetic and Bitwise Operators
      7. 3.7.5.7. Append
      8. 3.7.5.8. Data Lookups
  8. 3.8. Dynamic Typing
  9. 3.9. Coercions