The Lean Language Reference 日本語訳🔗

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

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

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

This reference manual is not yet complete, but there's enough information to provide value to users. The top priority is to add the missing information as quickly as possible while staying up to date with Lean development. As the rest of the text is written, regular snapshots will be released, tracking upstream changes. This snapshot covers Lean version 4.16.0-rc2.

Our prioritization of content is based on our best understanding of our users' needs. Please use the issue tracker to help us better understand what you need to know. In particular, please create or upvote issues for topics that are important to you. Your feedback is much appreciated! Once sufficient content is available, we will begin saving snapshots for each release of Lean and making them conveniently available.

API reference documentation is included from the Lean standard library source code. Due to technical limitations at the moment, the Lean terms and examples embedded in it do not render as nicely as we would like. In the near future, we will be working on removing these limitations. Additionally, we will be adding missing API reference documentation and revising and improving the existing API reference documentation.

Release History

2024-12-16

This is the initial release of the reference manual.

  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. 型システム（The Type System）
    1. 3.1. 関数（Functions）
    2. 3.2. 命題（Propositions）
    3. 3.3. 宇宙（Universes）
    4. 3.4. 帰納型（Inductive Types）
    5. 3.5. Quotients
  4. 4. ソースファイル（Source Files）
    1. 4.1. ファイル（Files）
    2. 4.2. モジュールの内容（Module Contents）
    3. 4.3. Axioms
    4. 4.4. Attributes
    5. 4.5. Dynamic Typing
    6. 4.6. Coercions
  5. 5. 再帰定義（Recursive Definitions）
    1. 5.1. Mutual Recursion
    2. 5.2. 構造的再帰（Structural Recursion）
    3. 5.3. Well-Founded Recursion
    4. 5.4. Partial and Unsafe Recursive Definitions
    5. 5.5. Controlling Reduction
  6. 6. 項（Terms）
    1. 6.1. 識別子（Identifiers）
    2. 6.2. 関数型（Function Types）
    3. 6.3. 関数（Functions）
    4. 6.4. 関数適用（Function Application）
    5. 6.5. リテラル（Literals）
    6. 6.6. 構造体とコンストラクタ（Structures and Constructors）
    7. 6.7. 条件（Conditionals）
    8. 6.8. パターンマッチ（Pattern Matching）
    9. 6.9. ホール（Holes）
    10. 6.10. Type Ascription
    11. 6.11. Quotation と Antiquotation（Quotation and Antiquotation）
    12. 6.12. do 記法（do-Notation）
    13. 6.13. 証明（Proofs）
  7. 7. 型クラス（Type Classes）
    1. 7.1. クラス定義（Class Declarations）
    2. 7.2. インスタンスの宣言（Instance Declarations）
    3. 7.3. インスタンス統合（Instance Synthesis）
    4. 7.4. インスタンス導出（Deriving Instances）
    5. 7.5. 基本的なクラス（Basic Classes）
  8. 8. 関手・モナド・do記法（Functors, Monads and do-Notation）
    1. 8.1. 規則（Laws）
    2. 8.2. モナドの持ち上げ（Lifting Monads）
    3. 8.3. 構文（Syntax）
    4. 8.4. API リファレンス（API Reference）
    5. 8.5. さまざまなモナド（Varieties of Monads）
  9. 9. IO
    1. 9.1. 論理モデル（Logical Model）
    2. 9.2. 制御構造（Control Structures）
    3. 9.3. コンソール出力（Console Output）
    4. 9.4. 可変参照（Mutable References）
    5. 9.5. ファイル・ファイルハンドラ・ストリーム（Files, File Handles, and Streams）
    6. 9.6. 環境変数（Environment Variables）
    7. 9.7. タイミング（Timing）
    8. 9.8. プロセス（Processes）
    9. 9.9. 乱数（Random Numbers）
    10. 9.10. Tasks and Threads
  10. 10. タクティクによる証明（Tactic Proofs）
    1. 10.1. タクティクの実行（Running Tactics）
    2. 10.2. 証明状態の読み方（Reading Proof States）
    3. 10.3. タクティク言語（The Tactic Language）
    4. 10.4. オプション
    5. 10.5. タクティクリファレンス（Tactic Reference）
    6. 10.6. conv によるターゲットの書き換え（Targeted Rewriting with conv ）
    7. 10.7. カスタムタクティク（Custom Tactics）
  11. 11. 単純化器（The Simplifier）
    1. 11.1. 単純化器の呼び出し（Invoking the Simplifier）
    2. 11.2. 書き換え規則（Rewrite Rules）
    3. 11.3. simp セット（Simp sets）
    4. 11.4. simp 正規形（Simp Normal Forms）
    5. 11.5. 終端・非終端位置（Terminal vs Non-Terminal Positions）
    6. 11.6. 単純化の設定（Configuring Simplification）
    7. 11.7. 単純化と書き換え（Simplification vs Rewriting）
  12. 12. 基本的な型（Basic Types）
    1. 12.1. 自然数（Natural Numbers）
    2. 12.2. Integers
    3. 12.3. Finite Natural Numbers
    4. 12.4. Fixed-Precision Integer Types
    5. 12.5. Bitvectors
    6. 12.6. Floating-Point Numbers
    7. 12.7. 文字（Characters）
    8. 12.8. 文字列（Strings）
    9. 12.9. ユニット型（The Unit Type）
    10. 12.10. The Empty Type
    11. 12.11. 真偽値（Booleans）
    12. 12.12. Optional Values
    13. 12.13. Tuples
    14. 12.14. Sum Types
    15. 12.15. Dependent Pairs
    16. 12.16. Linked Lists
    17. 12.17. 配列（Arrays）
    18. 12.18. Subtypes
    19. 12.19. Lazy Computations
    20. 12.20. Tasks and Threads
  13. 13. Standard Library
  14. 14. 記法とマクロ（Notations and Macros）
    1. 14.1. カスタム演算子（Custom Operators）
    2. 14.2. 優先順位（Precedence）
    3. 14.3. 記法（Notations）
    4. 14.4. 新しい構文の定義（Defining New Syntax）
    5. 14.5. マクロ（Macros）
    6. 14.6. Elaborators
  15. 15. Output from Lean
  16. 16. Elan
  17. 17. Lake and Reservoir
    1. 17.1. Lake
    2. 17.2. Reservoir
  18. Index
  19. 18. この翻訳について