The Lean Language Reference 日本語訳🔗

注意: この翻訳は有志による 非公式 翻訳です。原文の最新版は こちら です。

CAUTION: This is an Unofficial translation by volunteers. The latest version of original is here.

本書は Lean 言語リファレンス であり、Lean に関する執筆中のリファレンスです。本書は Lean についての包括的で正確な説明であることを意図しています：Lean のユーザが詳細な情報を調べることができる参考文献であって、新しいユーザのためのチュートリアルではありません。その他の文書については Lean のドキュメントサイト を参照してください。

  1. 1. はじめに（Introduction）
    1. 1.1. Lean
    2. 1.2. 表記規則（Typographical Conventions）
  2. 2. エラボレーションとコンパイル（Elaboration and Compilation）
    1. 2.1. パース（Parsing）
    2. 2.2. マクロ展開とエラボレーション（Macro Expansion and Elaboration）
    3. 2.3. カーネル（The Kernel）
    4. 2.4. エラボレーションの結果（Elaboration Results）
    5. 2.5. 初期化（Initialization）
  3. 3. Lean 言語について（The Lean Language）
    1. 3.1. ファイル（Files）
    2. 3.2. 型システム（The Type System）
    3. 3.3. モジュールの内容（Module Contents）
    4. 3.4. Axioms
    5. 3.5. Recursive Definitions
    6. 3.6. Attributes
    7. 3.7. Type Classes
    8. 3.8. Dynamic Typing
    9. 3.9. Coercions
  4. 4. Terms
  5. 5. Monads and do-Notation
  6. 6. IO
  7. 7. タクティクによる証明（Tactic Proofs）
    1. 7.1. タクティクの実行（Running Tactics）
    2. 7.2. 証明状態の読み方（Reading Proof States）
    3. 7.3. タクティク言語（The Tactic Language）
    4. 7.4. オプション
    5. 7.5. タクティクリファレンス（Tactic Reference）
    6. 7.6. conv によるターゲットの書き換え（Targeted Rewriting with conv ）
    7. 7.7. カスタムタクティク（Custom Tactics）
  8. 8. 単純化器（The Simplifier）
    1. 8.1. 単純化器の呼び出し（Invoking the Simplifier）
    2. 8.2. 書き換え規則（Rewrite Rules）
    3. 8.3. simp セット（Simp sets）
    4. 8.4. simp 正規形（Simp Normal Forms）
    5. 8.5. 終端・非終端位置（Terminal vs Non-Terminal Positions）
    6. 8.6. 単純化の設定（Configuring Simplification）
    7. 8.7. 単純化と書き換え（Simplification vs Rewriting）
  9. 9. 基本的な型（Basic Types）
    1. 9.1. 自然数（Natural Numbers）
    2. 9.2. Integers
    3. 9.3. Fixed-Precision Integer Types
    4. 9.4. Bitvectors
    5. 9.5. Floating-Point Numbers
    6. 9.6. 文字（Characters）
    7. 9.7. 文字列（Strings）
    8. 9.8. Linked Lists
    9. 9.9. Arrays
    10. 9.10. Lazy Computations
    11. 9.11. Tasks and Threads
  10. 10. Standard Library
    1. 10.1. Optional Values
  11. 11. Notations and Macros
    1. 11.1. Custom Operators
    2. 11.2. Precedence
    3. 11.3. Notations
    4. 11.4. Defining New Syntax
    5. 11.5. Macros
    6. 11.6. Elaborators
  12. 12. Output from Lean
  13. 13. Elan
  14. 14. Lake and Reservoir
    1. 14.1. Lake
    2. 14.2. Reservoir
  15. Index
  16. 15. この翻訳について