ハブは：
- https://leanprover.github.io/documentation/
- → Lean4のマニュアル作業中、現状は参考になっても参照はしないだろう。
- → Learning Lean すぐ下
- https://leanprover-community.github.io/learn.html
- https://leanprover.github.io/publications/
- https://leanprover-community.github.io/mathlib_docs/ mathlib doc
基本は：
だが、項目だけあって中身が空（未完成）のときがある。
例：型クラス
そんなときは：
- https://leanprover.github.io/theorem_proving_in_lean/type_classes.html これを見る 型クラス
- https://leanprover.github.io/lean4/doc/typeclass.html Lean4 の型クラス
- 『ヒッチハイカーのガイド』（ローカルにある ~/archive/Lean_hitchhikers_guide.pdf）を見る。https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf ← ダウンロードURL
例：コンバージョン
- https://leanprover.github.io/reference/tactics.html#conversions コンバージョンの記述がない
- https://leanprover-community.github.io/extras/conv.html コミュニティの文書にあった。
- https://leanprover.github.io/reference/metaprogramming.html 何もない。
- https://leanprover-community.github.io/extras/tactic_writing.html コミュニティ文書にあった。
- 『ヒッチハイカーのガイド』（ローカルにある ~/archive/Lean_hitchhikers_guide.pdf）の7章を見る。
- https://leanprover.github.io/papers/tactic.pdf 論文PDF
- Metaprogramming in Lean Youtube動画6本
