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

Lean by Example

ランダムぺージ