1. はじめに
  2. リンク集
  3. Mathlib4 Help
  4. ランダムページ
  7. 対話的コマンド
    ❱
    1. #check_failure: 意図的なエラー
    2. #check: 型を調べる
    3. #eval: 式を評価する
    4. #find: ライブラリ検索
    5. #guard_msgs: メッセージのテスト
    6. #guard: Bool 値のテスト
    7. #help: ドキュメントを見る
    8. #html: HTMLをインフォビューに表示
    9. #instances: インスタンスを列挙
    10. #lint: リンタ実行
    11. #loogle: Loogleで検索
    12. #print: 中身を見る
    13. #reduce: 式を簡約する
    14. #synth: 型クラスの検査
    15. #test: プロパティベーステスト
    16. #time: 実行時間計測
    17. #version: バージョン表示
    18. #whnf: 式を弱頭正規形に
  9. 宣言的コマンド
    ❱
    1. abbrev: 略称を定義する
    2. add_aesop_rules: aesop 改造
    3. attribute: 属性を付与する
    4. axiom: 公理を宣言する
    5. class: 型クラスを定義する
    6. declare_aesop_rule_sets: Aesopでタクティク自作
    7. declare_syntax_cat: 構文カテゴリ
    8. def: 関数などを定義する
    9. deriving: インスタンス自動生成
    10. dsimproc: simproc を宣言
    11. elab: 構文に意味を与える
    12. example: 名前をつけずに証明
    13. export: 現在の名前空間に追加
    14. inductive: 帰納型を定義する
    15. infix: 中置記法
    16. infixl: 左結合の中置記法
    17. infixr: 右結合の中置記法
    18. instance: インスタンスを定義する
    19. macro_rules: マクロ展開を定義
    20. macro: マクロの構文と解釈を定義
    21. mutual: 相互再帰
    22. namespace: 名前空間を宣言する
    23. notation: 記法を導入する
    24. opaque: 簡約できない名前を宣言
    25. open: 名前空間を開く
    26. postfix: 後置記法
    27. prefix: 前置記法
    28. proof_wanted: 証明を公募する
    29. register_label_attr: 属性自作
    30. register_option: オプション自作
    31. register_simp_attr: simpでタクティク自作
    32. section: 有効範囲を制限する
    33. set_option: オプション設定
    34. simproc: simproc を宣言
    35. structure: 構造体を定義する
    36. syntax: 構文を定義
    37. theorem: 命題を証明する
    38. variable: 引数を共通化する
  11. 修飾子
    ❱
    1. /-- -/: ドキュメントコメント
    2. decreasing_by: 関数の停止性を示す
    3. local: 有効範囲をセクションで限定
    4. noncomputable: 計算不能にする
    5. partial_fixpoint: 証明に使える部分関数を定義する
    6. partial: 部分関数を定義する
    7. private: 定義を不可視にする
    8. protected: フルネームを強制する
    9. scoped: 有効範囲を名前空間で限定
    10. termination_by: 再帰の進捗指標を指定
    11. unsafe: Leanのルールを破る
    12. where: 補助定義を追加
  13. 構文
    ❱
    1. ⟨x₁, x₂, .., xₙ⟩: 無名コンストラクタ
    2. [x₁, x₂, .., xₙ]: リストリテラル
    3. {x : T // p x}: 部分型
    4. {x y : A}: 暗黙の引数
    5. #[x₁, x₂, .., xₙ]: 配列リテラル
    6. ∀: 依存関数型
    7. |>: パイプライン演算子
    8. at h: タクティクの書き換え先を指定
    9. by: タクティクモードに入る
    10. e.f: フィールド記法
    11. match .. with: パターンマッチ
    12. panic!: エラーメッセージを出す
    13. s!: 文字列補間
    14. show .. from: 項の型を明示
    15. Σ: 依存ペア型
  15. 属性
    ❱
    1. aesop: aesop カスタマイズ
    2. app_unexpander: #checkコマンドやinfoviewでの表示を変更
    3. cases_eliminator: 独自場合分け
    4. coe: 型強制 ↑ として表示させる
    5. command_elab: コマンドの構文と実装の紐づけ
    6. csimp: 効率的な実装に置換
    7. default_instance: デフォルトの解決法
    8. elab_as_elim: 除去子として扱わせる
    9. implemented_by: 仕様と実装の分離
    10. induction_eliminator: 独自帰納法
    11. inherit_doc: ドキュメントの継承
    12. irreducible: 定義に展開できなくする
    13. macro_inline: 短絡評価など
    14. macro: マクロの構文と実装の紐づけ
    15. match_pattern: 独自パタンマッチ
    16. simp: 単純化ルール登録
    17. simps: simp 補題の自動生成
    18. tactic: タクティクの構文と実装の紐づけ
  17. オプション
    ❱
    1. autoImplicit: 自動束縛暗黙引数
    2. hygiene: マクロ衛生
    3. linter.flexible: 脆弱な証明を指摘する
    4. linter.style.multiGoal: フォーカス強制
    5. pp.macroStack: マクロ展開過程を表示
    6. relaxedAutoImplicit: 更にautoImplicit
    7. skipKernelTC: 型検査をスキップ
  19. 型クラス
    ❱
    1. Add: 閉じた + 演算用の記法クラス
    2. Alternative: 回復可能な失敗
    3. Applicative: アプリカティブ関手
    4. Coe: 型強制
    5. CoeDep: 依存型強制
    6. CoeFun: 関数型への強制
    7. CoeSort: 型宇宙への強制
    8. Decidable: 決定可能
    9. Functor: 関手
    10. GetElem: n番目の要素を取得
    11. HAdd: 一般の + 演算用の記法クラス
    12. HMul: 一般の * 演算用の記法クラス
    13. Inhabited: 有項にする
    14. LawfulFunctor: 関手則
    15. Monad: モナド
    16. Mul: 閉じた * 演算用の記法クラス
    17. Neg: - 演算用の記法クラス
    18. OfNat: 数値リテラルを使用
    19. Quote: クォート
    20. Repr: #eval の出力を表示
    21. Setoid: 同値関係
    22. ToString: 文字列に変換
  21. データ型
    ❱
    1. Array: 配列
    2. Async: 非同期計算
    3. Bool: 真偽値
    4. Char: Unicode 文字
    5. CommandElab: コマンドの実装
    6. Expr: 抽象構文木
    7. Float: 浮動小数点数
    8. HashMap: キーと値のペア
    9. HashSet: 重複を許さない集まり
    10. IO: 入出力
    11. Linter: リンター
    12. List: 連結リスト
    13. Macro: マクロの実装
    14. MLList: モナド多相遅延リスト
    15. Nat: 自然数
    16. Option: 失敗するかもしれない計算
    17. Prod: 型の積
    18. Prop: 命題全体
    19. Quotient: 同値関係による商
    20. String: 文字列
    21. Subtype: 部分型
    22. Sum: 型の和
    23. Syntax: 具象構文木
    24. Tactic: タクティクの実装
    25. Type: 型の型
    26. Vector: 長さ固定の配列
  23. タクティク
    ❱
    1. <;>: 生成された全ゴールに適用
    2. ac_rfl: 可換性と結合性を使う
    3. aesop: 自明な証明の自動探索
    4. all_goals: 全ゴールに対して適用
    5. apply at: apply を仮定に適用する
    6. apply_assumption: 自動 apply
    7. apply: 含意→を使う
    8. apply?: apply できるか検索
    9. assumption: 仮定を自動で exact
    10. by_cases: 排中律
    11. by_contra: 背理法
    12. calc: 計算モードに入る
    13. cases: 場合分けをする
    14. cases': Lean3版のcases
    15. choose: 選択関数を得る
    16. clear: 命題や定義を削除する
    17. congr: ゴールの関数適用を外す
    18. constructor: 論理積や同値性を示す
    19. contradiction: 矛盾を指摘
    20. contrapose: 対偶をとる
    21. conv: 変換モードに入る
    22. convert: 惜しい補題を使う
    23. decide: 決定可能な命題を示す
    24. done: 証明終了を宣言
    25. dsimp: 定義に展開
    26. exact: 証明を直接構成
    27. exact?: exact できるか検索
    28. exfalso: 矛盾を示すことに帰着
    29. exists: 存在∃を示す
    30. ext: 外延性を使う
    31. field_simp: 分母を払う
    32. fin_cases: 場合分けを簡潔に行う
    33. fun_induction: 関数に応じた帰納法
    34. fun_prop: 関数の諸性質を示す
    35. funext: 関数等式を示す
    36. gcongr: 合同性を用いる
    37. generalize: 一般化する
    38. grind: 証明自動化
    39. guard_hyp: 仮定や補題を確認
    40. have: 補題を用意する
    41. hint: 複数のタクティクを同時に試す
    42. induction: 帰納法
    43. induction': inductionの構文違い
    44. intro: 含意→や全称∀を示す
    45. itauto: 直観主義論理の枠内で示す
    46. left: 論理和∨を示す
    47. linarith: 線形(不)等式を示す
    48. native_decide: 実行による証明
    49. nlinarith: 非線形な(不)等式を示す
    50. norm_cast: 型キャストの簡略化
    51. nth_rw: n 番目の項だけ rw
    52. obtain: 分解して取り出す
    53. omega: 自然数の線形計画を解く
    54. order: 順序関係を扱う
    55. plausible: 反例を見つける
    56. positivity: 正値性を示す
    57. push_cast: 型キャストを内側へ
    58. push_neg: ドモルガン
    59. qify: 有理数にキャストする
    60. rcases: パターン分解
    61. refine: 穴埋め推論
    62. rel: 不等式を使う
    63. rename_i: 死んだ変数に名前を付ける
    64. repeat: 繰り返し適用
    65. replace: 補題の入れ替え
    66. revert: introの逆
    67. rfl: 定義に展開して等式を示す
    68. right: 論理和∨を示す
    69. ring_nf: 可換(半)環の標準形に
    70. ring: 可換(半)環の等式を示す
    71. rw_search: rw で示せるか検索
    72. rw: 同値変形
    73. says: タクティク提案の痕跡を残す
    74. set: 定義の導入
    75. show_term: タクティクの中身を出す
    76. show: 示すべきことを宣言
    77. simp_all: 仮定とゴールを全て単純化
    78. simp: 単純化
    79. sorry: 証明したことにする
    80. split: if/match 式を分解
    81. suffices: 十分条件に帰着
    82. tauto: トートロジーを示す
    83. trans: 推移律を利用する
    84. trivial: 基本的なタクティクを試す
    85. try: 失敗をエラーにしない
    86. unfold: 定義に展開
    87. use: 存在∃を示す
    88. with_reducible: 透過度指定
    89. wlog: 一般性を失わずに特殊化
    90. zify: 整数にキャストする