leanchecker¶
通常の開発では，lean や lake build によって各宣言がカーネルで検査されます．
さらに .olean に保存された環境を再検査するための道具として leanchecker があります．
概念的には，次のように使います．
通常の授業や演習ではここまで行う必要はありません．
ただし，「Lean の信頼は最終的に小さなカーネル検査に帰着する」という話をするときに，
.olean と leanchecker は重要なキーワードです．