コマンドライン：
- lean --print-prefix
- lean --print-libdir
- lake print-paths | jq .
- jq . ./lake-manifest.json
- cat .git/HEAD
- cat ~/.elan/update-hashes/* | sort
エディタ：
- #eval Lean.findOLean `Name
- #check と #eval で InfoViewをよく見る。
- set_option （下）
set_option trace.Elab.definition true set_option pp.universes false set_option pp.notation false set_option pp.coercions true
