6. 項（Terms）🔗

Planned Content

This chapter will describe Lean's term language, including the following features:

  • Name resolution, including variable occurrences, open declarations and terms

  • fun, with and without pattern matching

  • Literals (some via cross-references to the appropriate types, e.g. String)

Tracked at issue #66

項 （term）は Lean で数学やプログラムを書くための主要な手段です。 エラボレータ によって Lean の最小限のコア言語に翻訳・カーネルによってチェック・そして実行のためにコンパイルされます。項の構文は、 任意に拡張可能です ；本章では Lean にデフォルトで備わっている項の構文を説明します。

  1. 6.1. 識別子（Identifiers）
    1. 6.1.1. 先頭の（Leading .）
  2. 6.2. 関数型（Function Types）
  3. 6.3. 関数（Functions）
    1. 6.3.1. 暗黙のパラメータ（Implicit Parameters）
  4. 6.4. 関数適用（Function Application）
    1. 6.4.1. 一般化されたフィールド記法（Generalized Field Notation）
    2. 6.4.2. パイプライン構文（Pipeline Syntax）
  5. 6.5. リテラル（Literals）
    1. 6.5.1. 自然数（Natural Numbers）
    2. 6.5.2. 科学的数値（Scientific Numbers）
    3. 6.5.3. 文字列（Strings）
    4. 6.5.4. リストと配列（Lists and Arrays）
  6. 6.6. 構造体とコンストラクタ（Structures and Constructors）
  7. 6.7. 条件（Conditionals）
  8. 6.8. パターンマッチ（Pattern Matching）
    1. 6.8.1. 型（Types）
      1. 6.8.1.1. パターンの等価性の証明（Pattern Equality Proofs）
      2. 6.8.1.2. 明示的な動機（Explicit Motives）
      3. 6.8.1.3. 判別子の絞り込み（Discriminant Refinement）
      4. 6.8.1.4. 一般化（Generalization）
    2. 6.8.2. カスタムのパターン関数（Custom Pattern Functions）
    3. 6.8.3. パターンマッチ関数（Pattern Matching Functions）
    4. 6.8.4. その他のパターンマッチ演算子（Other Pattern Matching Operators）
    5. 6.8.5. Elaborating 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）