11. 単純化器(The Simplifier)🔗

単純化器は Lean で最もよく使われる機能の1つです。これは単純化規則のデータベースに基づいて、項を隅から隅まで書き換えます。単純化器は高度に設定可能であり、多くのタクティクが様々な方法で単純化器を使用しています。

  1. 11.1. 単純化器の呼び出し(Invoking the Simplifier)
    1. 11.1.1. パラメータ(Parameters)
  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)
    1. 11.6.1. オプション(Options)
  7. 11.7. 単純化と書き換え(Simplification vs Rewriting)