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